The following pages link to OTTER (Q15442):
Displaying 50 items.
- Automatic proofs and counterexamples for some ortholattice identities (Q293265) (← links)
- Case splitting in an automatic theorem prover for real-valued special functions (Q352970) (← links)
- First-order logic formalisation of impossibility theorems in preference aggregation (Q373021) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- Complex algebras of subalgebras (Q431656) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- A calculus for four-valued sequential logic (Q549178) (← links)
- Ken Kunen: algebraist. (Q649602) (← links)
- On different structure-preserving translations to normal form (Q674761) (← links)
- Automated discovery of new axiomatizations of the left group and right group calculi (Q688546) (← links)
- Experiments with discrimination-tree indexing and path indexing for term retrieval (Q688554) (← links)
- Single axioms for groups (Q688567) (← links)
- Single axioms for the left group and right group calculi (Q689202) (← links)
- Automation methods for logical derivation and their application in the control of dynamic and intelligent systems (Q742012) (← links)
- Problem corner: Robbins algebra: Conditions that make a near-Boolean algebra Boolean (Q751313) (← links)
- The problem of choosing the type of subsumption to use (Q809628) (← links)
- Double-negation elimination in some propositional logics (Q813082) (← links)
- Rectangular quasigroups and rectangular loops. (Q814030) (← links)
- Logic-based subsumption architecture (Q814558) (← links)
- Levi's commutator theorems for cancellative semigroups. (Q818943) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- On the separability of subproblems in Benders decompositions (Q846136) (← links)
- Power-associative, conjugacy closed loops. (Q855331) (← links)
- Uniqueness of Steiner laws on cubic curves (Q860106) (← links)
- Octopus: combining learning and parallel search (Q861370) (← links)
- Searching for shortest single axioms for groups of exponent \(6\) (Q861707) (← links)
- Mathematical induction in Otter-lambda (Q861715) (← links)
- \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) (Q867665) (← links)
- Steps toward a computational metaphysics (Q877243) (← links)
- Axiomatizing the skew Boolean propositional calculus (Q877820) (← links)
- Defining answer classes using resolution refutation (Q881832) (← links)
- Meeting the challenge of fifty years of logic (Q911807) (← links)
- MetiTarski: An automatic theorem prover for real-valued special functions (Q972422) (← links)
- Exploiting functional dependencies in declarative problem specifications (Q1028967) (← links)
- Automated verification of refinement laws (Q1037397) (← links)
- First order Stålmarck. Universal lemmas through branch merges (Q1040785) (← links)
- The linked inference principle. I: The formal treatment (Q1189727) (← links)
- A semantic backward chaining proof system (Q1193483) (← links)
- Single identities for lattice theory and for weakly associative lattices (Q1272238) (← links)
- Automating the search for elegant proofs (Q1272613) (← links)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis (Q1281504) (← links)
- The hot list strategy (Q1285861) (← links)
- The kernel strategy and its use for the study of combinatory logic (Q1311399) (← links)
- Single axioms for groups and abelian groups with various operations (Q1312155) (← links)
- SET-VAR (Q1319383) (← links)
- Uniform strategies: The CADE-11 theorem proving contest (Q1319384) (← links)
