A calculus for generating ground explanations

DOI10.1007/978-3-642-31365-3_17zbMATH Open1358.68189arXiv1201.5954OpenAlexW37301688MaRDI QIDQ2908490FDOQ2908490

Authors: Mnacho Echenim, Nicolas Peltier 

Publication date: 5 September 2012

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

Abstract: We present a modification of the superposition calculus that is meant to generate explanations why a set of clauses is satisfiable. This process is related to abductive reasoning, and the explanations generated are clauses constructed over so-called abductive constants. We prove the correctness and completeness of the calculus in the presence of redundancy elimination rules, and develop a sufficient condition guaranteeing its termination; this sufficient condition is then used to prove that all possible explanations can be generated infinite time for several classes of clause sets, including many of interest to the SMT community. We propose a procedure that generates a set of explanations that should be useful to a human user and conclude by suggesting several extensions to this novel approach.

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

Recommendations

• A superposition calculus for abductive reasoning
• On computing all abductive explanations from a propositional Horn theory
• The generation of abductive explanations from inconsistent theories
• Superposition with equivalence reasoning and delayed clause normal form transformation.
• Computer Science Logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cited In (2)

• Explanatory relations in arbitrary logics based on satisfaction systems, cutting and retraction
• A superposition calculus for abductive reasoning

This page was built for publication: A calculus for generating ground explanations

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