Backdoors to Abduction
Abductive reasoning (or Abduction, for short) is among the most fundamental AI reasoning methods, with a broad range of applications, including fault diagnosis, belief revision, and automated planning. Unfortunately, Abduction is of high computational complexity; even propositional Abduction is \Sigma_2^P-complete and thus harder than NP and coNP. This complexity barrier rules out the existence of a polynomial transformation to propositional satisfiability (SAT). In this work we use structural properties of the Abduction instance to break this complexity barrier. We utilize the problem structure in terms of small backdoor sets. We present fixed-parameter tractable transformations from Abduction to SAT, which make the power of today's SAT solvers available to Abduction.
Code (0)
등록된 구현이 없습니다.
Tasks
Fault DiagnosisSimilar Papers 제목 키워드 기반
ABox Abduction for Inconsistent Knowledge Bases under Repair Semantics
Given a knowledge base (KB) with a non-entailed fact, the ABox abduction problem asks for possible extensions of the KB that would entail this fact. This problem has many applications, ranging from diagnosis to explainab…
Propositional Abduction with Implicit Hitting Sets
Logic-based abduction finds important applications in artificial intelligence and related areas. One application example is in finding explanations for observed phenomena. Propositional abduction is a restriction of abdu…
Signature-Based Abduction with Fresh Individuals and Complex Concepts for Description Logics (Extended Version)
Given a knowledge base and an observation as a set of facts, ABox abduction aims at computing a hypothesis that, when added to the knowledge base, is sufficient to entail the observation. In signature-based ABox abductio…
Signature-Based Abduction for Expressive Description Logics -- Technical Report
Signature-based abduction aims at building hypotheses over a specified set of names, the signature, that explain an observation relative to some background knowledge. This type of abduction is useful for tasks such as di…
Abduction Prover in Isabelle/HOL
Proof assistants based on expressive logics suffer limited automation for proof search, raising the cost of formal verification based on proof assistants. We address this problem by introducing the Abduction Prover for I…