Logic-based Abduction Reasoning Task

From GM-RKB
Jump to navigation Jump to search

An Logic-based Abduction Reasoning Task is a Abductive Reasoning Task that is based on a formal logic.



References

2019

  • (Wikipedia, 2019) ⇒ https://en.wikipedia.org/wiki/Abductive_reasoning#Logic-based_abduction Retrieved:2019-9-1.
    • In logic, explanation is accomplished through the use of a logical theory [math]\displaystyle{ T }[/math] representing a domain and a set of observations [math]\displaystyle{ O }[/math] . Abduction is the process of deriving a set of explanations of [math]\displaystyle{ O }[/math] according to [math]\displaystyle{ T }[/math] and picking out one of those explanations. For [math]\displaystyle{ E }[/math] to be an explanation of [math]\displaystyle{ O }[/math] according to [math]\displaystyle{ T }[/math] , it should satisfy two conditions:
      • [math]\displaystyle{ O }[/math] follows from [math]\displaystyle{ E }[/math] and [math]\displaystyle{ T }[/math] ;
      • [math]\displaystyle{ E }[/math] is consistent with [math]\displaystyle{ T }[/math] .
    • In formal logic, [math]\displaystyle{ O }[/math] and [math]\displaystyle{ E }[/math] are assumed to be sets of literals. The two conditions for [math]\displaystyle{ E }[/math] being an explanation of [math]\displaystyle{ O }[/math] according to theory [math]\displaystyle{ T }[/math] are formalized as: : [math]\displaystyle{ T \cup E \models O; }[/math] : [math]\displaystyle{ T \cup E }[/math] is consistent.

      Among the possible explanations [math]\displaystyle{ E }[/math] satisfying these two conditions, some other condition of minimality is usually imposed to avoid irrelevant facts (not contributing to the entailment of [math]\displaystyle{ O }[/math] ) being included in the explanations. Abduction is then the process that picks out some member of [math]\displaystyle{ E }[/math] . Criteria for picking out a member representing "the best" explanation include the simplicity, the prior probability, or the explanatory power of the explanation.

      A proof-theoretical abduction method for first order classical logic based on the sequent calculus and a dual one, based on semantic tableaux (analytic tableaux) have been proposed (Cialdea Mayer & Pirri 1993). The methods are sound and complete and work for full first order logic, without requiring any preliminary reduction of formulae into normal forms. These methods have also been extended to modal logic.

       Abductive logic programming is a computational framework that extends normal logic programming with abduction. It separates the theory [math]\displaystyle{ T }[/math] into two components, one of which is a normal logic program, used to generate [math]\displaystyle{ E }[/math] by means of backward reasoning, the other of which is a set of integrity constraints, used to filter the set of candidate explanations.

2017

2. [math]\displaystyle{ T \cup H }[/math] is consistent,
where [math]\displaystyle{ \models }[/math] denotes the deductive entailment relation of the formal logic used in the representation of our theory and consistency refers also to the corresponding notion in this logic. The particular choice of this underlying formal framework of logic is in general a matter that depends on the problem or phenomena that we are trying to model. In many cases, this is based on first order predicate calculus, as, for example, in the approach of theory completion in Muggleton and Bryant (2000). But other logics can be used, e.g., the nonmonotonic logics of default logic or logic programming with negation as failure when the modeling of our problem requires this level of expressivity.