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

DOI10.1007/978-3-319-24246-0_6zbMATH Open1471.03020arXiv1503.02971OpenAlexW1936712172MaRDI QIDQ2964455FDOQ2964455

Authors: Andreas Teucke, Christoph Weidenbach 

Publication date: 27 February 2017

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

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Combining superposition, sorts and splitting
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Title not available (Why is that?)
• A theory of abstraction
• Explicit representation of terms defined by counter examples
• Term-rewriting systems with rule priorities
• 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
• Title not available (Why is that?)
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• SCL clause learning from simple models
• On First-Order Model-Based Reasoning
• Automated reasoning building blocks
• Partial instantiation methods for inference in first-order logic
• Title not available (Why is that?)
• Types for Proofs and Programs
• Automatic models of first order theories

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)