Help Privacy Policy Disclaimer
  Advanced SearchBrowse





An Approximation and Refinement Approach to First-Order Automated Reasoning


Teucke,  Andreas
Automation of Logic, MPI for Informatics, Max Planck Society;
International Max Planck Research School, MPI for Informatics, Max Planck Society;

Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Teucke, A. (2018). An Approximation and Refinement Approach to First-Order Automated Reasoning. PhD Thesis, Universität des Saarlandes, Saarbrücken. doi:10.22028/D291-27196.

Cite as: http://hdl.handle.net/21.11116/0000-0001-8E49-E
With the goal of lifting model-based guidance from the propositional setting to first- order logic, I have developed an approximation theorem proving approach based on counterexample-guided abstraction refinement. A given clause set is transformed into a simplified form where satisfiability is decidable. This approximation extends the signature and preserves unsatisfiability: if the simplified clause set is satisfi- able, so is the original clause set. A resolution refutation generated by a decision procedure on the simplified clause set can then either be lifted to a refutation in the original clause set, or it guides a refinement excluding the previously found unliftable refutation. This way the approach is refutationally complete. The monadic shallow linear Horn fragment, which is the initial target of the approximation, is well-known to be decidable. It was a long standing open prob- lem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. I have now proven de- cidability of the non-Horn monadic shallow linear fragment via ordered resolution. I further extend the clause language with a new type of constraints, called straight dismatching constraints. The extended clause language is motivated by an improved refinement of the approximation-refinement framework. All needed oper- ations on straight dismatching constraints take linear or linear logarithmic time in the size of the constraint. Ordered resolution with straight dismatching constraints is sound and complete and the monadic shallow linear fragment with straight dis- matching constraints is decidable. I have implemented my approach based on the SPASS theorem prover. On cer- tain satisfiable problems, the implementation shows the ability to beat established provers such as SPASS, iProver, and Vampire.