A method for building models automatically. Experiments with an extension of OTTER

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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

• OTTER
• SATCHMO

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