Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
From MaRDI portal
Publication:4610336
DOI10.1007/BFb0027423zbMath1412.68253OpenAlexW1497875247MaRDI QIDQ4610336
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
automated theorem proverequational constraintdecision procedureequational formulapartial interpretation
Related Items
Uses Software
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