First-order logic theorem proving and model building via approximation and instantiation

DOI10.1007/978-3-319-24246-0_6MaRDI QIDQ2964455zbMATH OpenOpenAlexFDO

Authors Andreas Teucke, Christoph Weidenbach

Publication date 27 February 2017

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1503.02971

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Abstract: In this paper we consider first-order logic theorem proving and model building via approximation and instantiation. Given a clause set we propose its approximation into a simplified clause set where satisfiability is decidable. The approximation extends the signature and preserves unsatisfiability: if the simplified clause set is satisfiable in some model, so is the original clause set in the same model interpreted in the original signature. A 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. We do not step-wise lift refutations but conflicting cores, finite unsatisfiable clause sets representing at least one refutation. The approach is dual to many existing approaches in the literature because our approximation preserves unsatisfiability.

Recommendations

• SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
• Resolution theorem proving
• scientific article; zbMATH DE number 1841825
• scientific article; zbMATH DE number 1300967
• Refutational theorem proving for hierarchic first-order theories

Cites work

• scientific article; zbMATH DE number 1341618 (Why is no real title available?)
• A theory of abstraction
• Combining superposition, sorts and splitting
• Explicit representation of terms defined by counter examples
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Term-rewriting systems with rule priorities
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Theorem proving with abstraction

Cited in

(11)

• SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
• AVATAR: The Architecture for First-Order Theorem Provers
• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• SCL clause learning from simple models
• On First-Order Model-Based Reasoning
• Partial instantiation methods for inference in first-order logic
• Automated reasoning building blocks
• scientific article; zbMATH DE number 1301853 (Why is no real title available?)
• Automatic models of first order theories
• Types for Proofs and Programs

Describes a project that uses

Uses Software

• TPTP

This page was built for publication: First-order logic theorem proving and model building via approximation and instantiation

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