Superposition for fixed domains

DOI10.1145/1805950.1805957MaRDI QIDQ2946615zbMATH OpenOpenAlexFDO

Authors Matthias Horbach, Christoph Weidenbach

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

automated theorem provingfixed domain semanticsinductionless inductionminimal model semanticsproof by consistencysuperposition

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Abstract: Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the minimal model's term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired. Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and refutationally complete in the limit for a first-order fixed domain semantics. For saturated Horn theories and classes of positive formulas, we can even employ the calculus to prove properties of the minimal model itself, going beyond the scope of known superposition-based approaches.

Recommendations

• Superposition for Fixed Domains
• Superposition for bounded domains
• A superposition calculus for abductive reasoning
• Superposition modulo a Shostak theory.
• Superposition with equivalence reasoning and delayed clause normal form transformation.

Cited in

(13)

• Superposition decides the first-order logic fragment over ground theories
• A superposition calculus for abductive reasoning
• Combining induction and saturation-based theorem proving
• scientific article; zbMATH DE number 5857449 (Why is no real title available?)
• A rule-based framework for building superposition-based decision procedures
• Superposition modulo non-linear arithmetic
• Superposition for Fixed Domains
• Superposition for bounded domains
• Harald Ganzinger's legacy: contributions to logics and programming
• Semantics for first-order superposition logic
• Predicate Completion for non-Horn Clause Sets
• System description: SPASS-FD
• Superposition modulo a Shostak theory.

This page was built for publication: Superposition for fixed domains

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