OTTER

swMATH2904MaRDI QIDQ15442FDOQ15442

Author name not available (Why is that?)

Described by source

• Automatic theorem proving and OTTER

Cited In (only showing first 100 items - show all)

• Building Theorem Provers
• Automated reasoning with power maps
• The application of automated reasoning to formal models of combinatorial optimization
• Heaps and Data Structures: A Challenge for Automated Provers
• Old or heavy? Decaying gracefully with age/weight shapes
• A note on assumptions about Skolem functions
• A posthumous contribution by Larry Wos: excerpts from an unpublished column
• A Wos Challenge Met
• Larry Wos: visions of automated reasoning
• Set of support, demodulation, paramodulation: a historical perspective
• An efficient subsumption test pipeline for BS(LRA) clauses
• Retrieving geometric information from images: the case of hand-drawn diagrams
• Layered map reasoning: an experimental approach put to trial on sets
• On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
• History and Prospects for First-Order Automated Deduction
• When is the commutant of a Bol loop a subloop?
• First order logic with domain conditions
• Title not available (Why is that?)
• Three-variable statements of set-pairing
• Learning to solve geometric construction problems from images
• OTTER experiments in a system of combinatory logic
• A generic graphic framework for combining inference tools and editing proofs and formulae
• Computational Verification of Network Programs in Coq
• A comprehensive framework for saturation theorem proving
• Making higher-order superposition work
• Missing proofs found
• Title not available (Why is that?)
• Learning theorem proving components
• OTTER Proofs in Tarskian Geometry
• Substitution tree indexing
• Extending E Prover with Similarity Based Clause Selection Strategies
• Implementing Euclid's straightedge and compass constructions in type theory
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• Partial matching for analogy discovery in proofs and counter-examples
• Implementing Superposition in iProver (System Description)
• Limited second-order functionality in a first-order setting
• Title not available (Why is that?)
• Extended path-indexing
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Mechanizing Mathematical Reasoning
• MACE4 and SEM: a comparison of finite model generators
• Title not available (Why is that?)
• Distributivity in Ł\(_{\aleph_0}\) and other sentential logics
• Title not available (Why is that?)
• Gibbard's collapse theorem for the indicative conditional: an axiomatic approach
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Presenting inequations in mathematical proofs
• : A Resolution-Based Prover for Multimodal K
• Goals and benchmarks for automated map reasoning
• System Description: E.T. 0.1
• A model and a first analysis of distributed-search contraction-based strategies
• The legacy of a great researcher
• Title not available (Why is that?)
• The seventeen provers of the world. Foreword by Dana S. Scott..
• \(G\)-loops and permutation groups
• The resonance strategy
• Searching for shortest single axioms for groups of exponent \(6\)
• Title not available (Why is that?)
• Automated development of Tarski's geometry
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automating the search for elegant proofs
• The TPTP problem library
• On the separability of subproblems in Benders decompositions
• Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
• A calculus for four-valued sequential logic
• Clause trees: A tool for understanding and implementing resolution in automated reasoning
• Resolution-based methods for modal logics
• KI 2004: Advances in Artificial Intelligence
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Mechanizing Mathematical Reasoning
• Superposition for bounded domains
• Loops with abelian inner mapping groups: an application of automated deduction
• Uniqueness of Steiner laws on cubic curves
• Octopus: combining learning and parallel search
• Mathematical induction in Otter-lambda
• Supporting the formal verification of mathematical texts
• Layered clause selection for theory reasoning (short paper)
• Title not available (Why is that?)
• Title not available (Why is that?)
• SET-VAR
• The semantics of answer literals
• Comparing approaches to the exploration of the domain of residue classes.
• A note on monothetic BCI
• Steps toward a computational metaphysics
• Defining answer classes using resolution refutation
• Automation methods for logical derivation and their application in the control of dynamic and intelligent systems
• Click'n prove: interactive proofs within set theory
• Constraint solving for proof planning
• The structure of F-quasigroups.
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• Knowledge-based proof planning

This page was built for software: OTTER