SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment

DOI10.1007/S10817-020-09546-ZzbMATH Open1468.68308OpenAlexW3006784105MaRDI QIDQ2303255FDOQ2303255

Authors: Andreas Teucke, Christoph Weidenbach 

Publication date: 3 March 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-02965030/file/main.pdf

Recommendations

• First-order logic theorem proving and model building via approximation and instantiation
• SPASS \& FLOTTER version 0.42
• Resolution theorem proving
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• scientific article; zbMATH DE number 1300967

zbMATH Keywords

decidabilitymodel generationfirst-order theorem provingapproximation refinement

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Automated model building
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• AVATAR: The Architecture for First-Order Theorem Provers
• First-order logic theorem proving and model building via approximation and instantiation
• Ordered chaining calculi for first-order theories of transitive relations
• On the saturation of YAGO
• The model evolution calculus.
• Title not available (Why is that?)
• Deciding \(\mathcal H_1\) by resolution
• Term-rewriting systems with rule priorities
• Title not available (Why is that?)
• Extending \(H_1\)-clauses with disequalities
• Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses
• On the expressivity and applicability of model representation formalisms
• Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints
• Extending \({\mathcal H}_1\)-clauses with path disequalities
• Title not available (Why is that?)

Cited In (3)

• First-order atom definitions extended
• First-order logic theorem proving and model building via approximation and instantiation
• SPASS-AR

Uses Software

• VAMPIRE
• SPASS
• TPTP
• iProver
• YAGO
• AVATAR

This page was built for publication: SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2303255)