OTTER
From MaRDI portal
Cited in
(only showing first 100 items - show all)- scientific article; zbMATH DE number 1050895 (Why is no real title available?)
- Axiomatizing the skew Boolean propositional calculus
- The legacy of a great researcher
- An algorithm for the retrieval of unifiers from discrimination trees
- Subgoal strategies for solving board puzzles
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Automated reasoning with power maps
- The application of automated reasoning to formal models of combinatorial optimization
- scientific article; zbMATH DE number 1461245 (Why is no real title available?)
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- Building Theorem Provers
- A note on assumptions about Skolem functions
- Old or heavy? Decaying gracefully with age/weight shapes
- Heaps and Data Structures: A Challenge for Automated Provers
- \(G\)-loops and permutation groups
- scientific article; zbMATH DE number 2134000 (Why is no real title available?)
- Removing irrelevant information in temporal resolution proofs
- 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
- The resonance strategy
- scientific article; zbMATH DE number 1444729 (Why is no real title available?)
- On the desirability of mechanizing calculational proofs
- Logic for Programming, Artificial Intelligence, and Reasoning
- User interaction with the Matita proof assistant
- Tarski geometry axioms. III
- scientific article; zbMATH DE number 1865568 (Why is no real title available?)
- scientific article; zbMATH DE number 4160159 (Why is no real title available?)
- Computational verification of network programs in Coq
- Searching for shortest single axioms for groups of exponent \(6\)
- Proof search in a context-sensitive logic for molecular biology
- scientific article; zbMATH DE number 1524505 (Why is no real title available?)
- Scavenger 0.1: a theorem prover based on conflict resolution
- Retrieving geometric information from images: the case of hand-drawn diagrams
- Automatic derivation of the irrationality of \(e\)
- Automated development of Tarski's geometry
- Commutativity theorems in groups with power-like maps
- scientific article; zbMATH DE number 1765667 (Why is no real title available?)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Lemma matching for a PTTP-based top-down theorem prover
- Evolving combinators
- The TM system for repairing non-theorems
- scientific article; zbMATH DE number 1882060 (Why is no real title available?)
- Automating Algebraic Specifications of Non-freely Generated Data Types
- On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
- Layered map reasoning: an experimental approach put to trial on sets
- Presenting and explaining Mizar
- Towards the qualitative, plan-based simulation of international crises
- scientific article; zbMATH DE number 1254024 (Why is no real title available?)
- Computer proofs about finite and regular sets: The unifying concept of subvariance.
- Mathematical applications of inductive logic programming
- scientific article; zbMATH DE number 1696826 (Why is no real title available?)
- The disconnection method
- Automating the search for elegant proofs
- First order Stålmarck. Universal lemmas through branch merges
- scientific article; zbMATH DE number 1303345 (Why is no real title available?)
- scientific article; zbMATH DE number 2000435 (Why is no real title available?)
- scientific article; zbMATH DE number 2043541 (Why is no real title available?)
- Advances in Artificial Intelligence – SBIA 2004
- Finding proofs in Tarskian geometry
- On the separability of subproblems in Benders decompositions
- scientific article; zbMATH DE number 1859175 (Why is no real title available?)
- Semantic trees revisited: some new completeness results
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
- OTTER proofs in Tarskian geometry
- The TPTP problem library
- A calculus for four-valued sequential logic
- When is the commutant of a Bol loop a subloop?
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- First order logic with domain conditions
- SOLAR: a consequence finding system for advanced reasoning
- Filter-based resolution principle for lattice-valued propositional logic LP(X)
- The Relative Power of Semantics and Unification
- Computer and Human Reasoning: Single Implicative Axioms for Groups and for Abelian Groups
- scientific article; zbMATH DE number 1348483 (Why is no real title available?)
- A domain-independent system for modeling number theory using first-order predicate logic
- Linear groupoids and the associated wreath products.
- Resolution-based methods for modal logics
- scientific article; zbMATH DE number 7582520 (Why is no real title available?)
- 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
- Three-variable statements of set-pairing
- Automated theorem proving for special functions: the next phase
- scientific article; zbMATH DE number 1500560 (Why is no real title available?)
- scientific article; zbMATH DE number 1765674 (Why is no real title available?)
- Robbins algebras vs. Boolean algebras
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Principal rings and their invariant factors
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Ordered tableaux: extensions and applications
- Mechanizing Mathematical Reasoning
- A formal framework for managing mathematics
- Learning to solve geometric construction problems from images
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- On deciding satisfiability by theorem proving with speculative inferences
- Foundations of Information and Knowledge Systems
- Superposition for bounded domains
This page was built for software: OTTER
