A superposition calculus for abductive reasoning

DOI10.1007/S10817-015-9344-2zbMATH Open1433.03023arXiv1406.0303OpenAlexW1751510650MaRDI QIDQ2013317FDOQ2013317

Mnacho Echenim, Nicolas Peltier

Publication date: 17 August 2017

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

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.

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Term Rewriting and All That
• A rewriting approach to satisfiability procedures.
• Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings
• Automated model building
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• New results on rewrite-based satisfiability procedures
• Automatic decidability and combinability
• Paramodulation-based theorem proving
• Superposition Modulo Linear Arithmetic SUP(LA)
• Refutational theorem proving for hierarchic first-order theories
• RST Flip-Flop Input Equations
• An incremental method for generating prime implicants/implicates
• Equality and abductive residua for Horn clauses
• Hierarchic Superposition with Weak Abstraction
• Combination of convex theories: modularity, deduction completeness, and explanation
• Computer Aided Verification
• First order abduction via tableau and sequent calculi
• A Calculus for Generating Ground Explanations
• Automatic Decidability: A Schematic Calculus for Theories with Counting Operators
• Hierarchical Reasoning for the Verification of Parametric Systems
• Abduction in Logic Programming as Second-Order Quantifier Elimination
• A Rewriting Strategy to Generate Prime Implicates in Equational Logic
• Finite Quantification in Hierarchic Theorem Proving
• Prime Implicate Tries
• Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
• Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
• Computing prime implicants

Cited In (3)

• On structures of regular standard contradictions in propositional logic
• Super-Solutions
• Induction with generalization in superposition reasoning

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)