Skip to Main content Skip to Navigation
Journal articles

SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment

Andreas Teucke 1, 2 Christoph Weidenbach 1, 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We introduce FO-AR, an approximation-refinement approach for first-order theorem proving based on counterexample-guided abstraction refinement. A given first-order clause set N is transformed into an over-approximation N in a decidable first-order fragment. That means if N is satisfiable so is N. However, if N is unsatisfiable, then the approximation provides a lifting terminology for the found refutation which is step-wise transformed into a proof of unsatisfiability for N. If this fails, the cause is analyzed to refine the original clause set such that the found refutation is ruled out for the future and the procedure repeats. The target fragment of the transformation is the monadic shallow linear fragment with straight dismatching constraints, which we prove to be decidable via ordered resolution with selection. We further discuss practical aspects of SPASS-AR, a first-order theorem prover implementing FO-AR. We focus in particularly on effective algorithms for lifting and refinement.
Document type :
Journal articles
Complete list of metadatas

Cited literature [41 references]  Display  Hide  Download

https://hal.inria.fr/hal-02965030
Contributor : Christoph Weidenbach <>
Submitted on : Tuesday, October 13, 2020 - 2:47:56 PM
Last modification on : Saturday, October 24, 2020 - 3:37:59 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Andreas Teucke, Christoph Weidenbach. SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment. Journal of Automated Reasoning, Springer Verlag, 2020, 64 (3), pp.611-640. ⟨10.1007/s10817-020-09546-z⟩. ⟨hal-02965030⟩

Share

Metrics

Record views

12

Files downloads

56