OTTER

MaRDI QIDQ15442swMATHFDO

Official website https://www.mcs.anl.gov/research/projects/AR/otter/

Described by source

• Automatic theorem proving and OTTER

Cited in

(only showing first 100 items - show all)

• Exploiting functional dependencies in declarative problem specifications
• Automated verification of refinement laws
• First order Stålmarck. Universal lemmas through branch merges
• The linked inference principle. I: The formal treatment
• A semantic backward chaining proof system
• Single identities for lattice theory and for weakly associative lattices
• Automating the search for elegant proofs
• On the modelling of search in theorem proving -- towards a theory of strategy analysis
• The hot list strategy
• The kernel strategy and its use for the study of combinatory logic
• Single axioms for groups and abelian groups with various operations
• SET-VAR
• Uniform strategies: The CADE-11 theorem proving contest
• Automated proofs of equality problems in Overbeek's competition
• The problem of induction
• MetiTarski
• On subsumption in distributed derivations
• Problem solving by searching for models with a theorem prover
• The shortest single axioms for groups of exponent 4
• Single identities for ternary Boolean algebras
• Automated reasoning about cubic curves
• Towards automating duality
• The resonance strategy
• Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
• SETHEO
• lazyCoP
• A learning procedure for mathematics.
• The application of automated reasoning to questions in mathematics and logic
• The power of combining resonance with heat
• The semantics of answer literals
• Theorema
• TPS
• INGRID
• An algorithm for the retrieval of unifiers from discrimination trees
• Temporal resolution using a breadth-first search algorithm
• Subgoal strategies for solving board puzzles
• Shortest single axioms for the equivalential calculus with CD and RCD
• Automated deduction techniques for classification in description logic systems
• Hilberticus
• Clause trees: A tool for understanding and implementing resolution in automated reasoning
• Computing answers with model elimination
• Comparing approaches to the exploration of the domain of residue classes.
• Limited resource strategy in resolution theorem proving
• IeanCOP: lean connection-based theorem proving
• Computer proofs about finite and regular sets: The unifying concept of subvariance.
• lolliCoP
• Principal rings and their invariant factors
• OilEd
• Shortest axiomatizations of implicational S4 and S5
• PLAGIATOR
• TGTP
• THEO
• MizarMode
• SATLIB
• CAS/PI
• TAPS
• MPTP
• MPTP 0.2
• VAMPIRE
• Deciding the E^+-class by an a posteriori, liftable order
• Proofs as schemas and their heuristic use
• On middle distributivity for skew lattices
• Evaluating general purpose automated theorem proving systems
• On the desirability of mechanizing calculational proofs
• Towards the qualitative, plan-based simulation of international crises
• SPASS
• TPTP
• Darwin
• SPASS+T
• STRIP
• Automated conjecturing. III. Property-relations conjectures
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• LPL software
• Quantum B-algebras: their omnipresence in algebraic logic and beyond
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Prover9
• Retrieving geometric information from images: the case of hand-drawn diagrams
• A generalization of Moufang and Steiner loops.
• Constraint solving for proof planning
• ProofWatch: watchlist guidance for large theories in E
• Tarski geometry axioms. III
• OTTER and the Moufang identity problem
• Presenting inequations in mathematical proofs
• \(G\)-loops and permutation groups
• Automated development of Tarski's geometry
• FINDER
• The application of automated reasoning to formal models of combinatorial optimization
• Deciding the guarded fragments by resolution
• Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus
• SATCHMO
• DCTP
• I-SATCHMO
• SCOTT
• Three-variable statements of set-pairing
• E-Darvin
• MUSCADET
• Single axioms for odd exponent groups
• OTTER experiments in a system of combinatory logic
• A generic graphic framework for combining inference tools and editing proofs and formulae
• Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover

This page was built for software: OTTER