A superposition calculus for abductive reasoning

DOI10.1007/S10817-015-9344-2MaRDI QIDQ2013317zbMATH OpenOpenAlexFDO

Authors Mnacho Echenim, Nicolas Peltier

Publication date 17 August 2017

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

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

zbMATH Keywords

abductionsuperposition calculusdeductive-completenessequational first-order logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: We present a modification of the superposition calculus that is meant to generate consequences of sets of first-order axioms. This approach is proven to be sound and deductive-complete in the presence of redundancy elimination rules, provided the considered consequences are built on a given finite set of ground terms, represented by constant symbols. In contrast to other approaches, most existing results about the termination of the superposition calculus can be carried over to our procedure. This ensures in particular that the calculus is terminating for many theories of interest to the SMT community.

Recommendations

• A calculus for generating ground explanations
• A combined superposition and model evolution calculus
• Superposition and Model Evolution Combined
• Superposition for fixed domains
• Superposition for Fixed Domains

Cites work

• scientific article; zbMATH DE number 500950 (Why is no real title available?)
• scientific article; zbMATH DE number 976360 (Why is no real title available?)
• scientific article; zbMATH DE number 3231608 (Why is no real title available?)
• A calculus for generating ground explanations
• A rewriting approach to satisfiability procedures.
• A rewriting strategy to generate prime implicates in equational logic
• Abduction in logic programming as second-order quantifier elimination
• An incremental method for generating prime implicants/implicates
• Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings
• Automated model building
• Automatic decidability and combinability
• Automatic decidability: a schematic calculus for theories with counting operators
• Combination of convex theories: modularity, deduction completeness, and explanation
• Computer Aided Verification
• Computing prime implicants
• Equality and abductive residua for Horn clauses
• Finite Quantification in Hierarchic Theorem Proving
• First order abduction via tableau and sequent calculi
• Hierarchic superposition with weak abstraction
• Hierarchical reasoning and model generation for the verification of parametric hybrid systems
• Hierarchical reasoning for the verification of parametric systems
• New results on rewrite-based satisfiability procedures
• Paramodulation-based theorem proving
• Prime implicate tries
• RST Flip-Flop Input Equations
• Refutational theorem proving for hierarchic first-order theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
• Superposition modulo linear arithmetic SUP(LA)
• Term Rewriting and All That

Cited in

(5)

• Super-Solutions
• Superposition for fixed domains
• On structures of regular standard contradictions in propositional logic
• A calculus for generating ground explanations
• Superposition for Fixed Domains

Describes a project that uses

Uses Software

• Yices
• z3
• veriT

This page was built for publication: A superposition calculus for abductive reasoning

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