Simplifying and generalizing formulae in tableaux. Pruning the search space and building models

DOI10.1007/BFb0027423zbMath1412.68253OpenAlexW1497875247MaRDI QIDQ4610336

Nicolas Peltier

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bfb0027423

zbMATH Keywords

automated theorem proverequational constraintdecision procedureequational formulapartial interpretation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Combining enumeration and deductive techniques in order to increase the class of constructible infinite models

Uses Software

• FINDER
• SATCHMO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Equational problems and disunification
• Resolution methods for the decision problem
• Increasing model building capabilities by constraint solving on terms with integer exponents
• A-ordered tableaux
• Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
• A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
• Using resolution for deciding solvable classes and building finite models
• Minimal model generation with positive unit hyper-resolution tableaux
• Hyperresolution and automated model building
• A method for building models automatically. Experiments with an extension of OTTER
• Hyper tableaux
• Automatic Theorem Proving With Renamable and Semantic Resolution