A method for building models automatically. Experiments with an extension of OTTER
From MaRDI portal
Publication:5210763
DOI10.1007/3-540-58156-1_6zbMath1433.68536OpenAlexW1689813061MaRDI QIDQ5210763
Christophe Bourely, Nicolas Peltier, Ricardo Caferra
Publication date: 21 January 2020
Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-58156-1_6
Related Items (6)
A calculus combining resolution and enumeration for building finite models ⋮ Simplifying and generalizing formulae in tableaux. Pruning the search space and building models ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ Analogy in Automated Deduction: A Survey ⋮ A method for building models automatically. Experiments with an extension of OTTER ⋮ Building proofs or counterexamples by analogy in a resolution framework
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Equational problems and disunification
- A method for simultaneous search for refutations and models by equational constraint solving
- Decidability of a portion of the predicate calculus
- Resolution methods for the decision problem
- Automated Theorem Proving: After 25 Years
- Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
- A method for building models automatically. Experiments with an extension of OTTER
- Automatic Theorem Proving With Renamable and Semantic Resolution
This page was built for publication: A method for building models automatically. Experiments with an extension of OTTER