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
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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 metadata

Cited literature [41 references]  Display  Hide  Download

https://hal.inria.fr/hal-02965030
Contributor : Christoph Weidenbach Connect in order to contact the contributor
Submitted on : Tuesday, October 13, 2020 - 2:47:56 PM
Last modification on : Saturday, October 16, 2021 - 11:26:06 AM
Long-term archiving on: : Thursday, January 14, 2021 - 6:08:39 PM

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

49

Files downloads

175