Wyniki wyszukiwania - BazTech

1

The CHR-based Implementation of the SCIFF Abductive System

Alberti M., Gavanelli M., Lamma E.

Fundamenta Informaticae

|

2013

|

Vol. 124, nr 4

365--381

EN

Abduction is a form of inference that supports hypothetical reasoning and has been applied to a number of domains, such as diagnosis, planning, protocol verification. Abductive Logic Programming (ALP) is the integration of abduction in logic programming. Usually, the operational semantics of an ALP language is defined as a proof procedure. The first implementations of ALP proof-procedures were based on the meta-interpretation technique, which is flexible but limits the use of the built-in predicates of logic programming systems. Another, more recent, approach exploits theoretical results on the similarity between abducibles and constraints. With this approach, which bears the advantage of an easy integration with built-in predicates and constraints, Constraint Handling Rules has been the language of choice for the implementation of abductive proof procedures. The first CHR-based implementation mapped integrity constraints directly to CHR rules, which is an efficient solution, but prevents defined predicates from being in the body of integrity constraints and does not allow a sound treatment of negation by default. In this paper, we describe the CHR-based implementation of the SCIFF abductive proof-procedure, which follows a different approach. The SCIFF implementation maps integrity constraints to CHR constraints, and the transitions of the proof-procedure to CHR rules, making it possible to treat default negation, while retaining the other advantages of CHR-based implementations of ALP proof-procedures.

2

On Undecidability of Non-monotonic Logic

Suchenek M. A.

Studia Informatica : systems and information technology

|

2006

|

Vol. 1(7)

127--132

EN

The degree of undecidability of nonmonotonic logic is investigated. A proof is provided that arithmetical but not recursively enumerable sets of sentences definable by nonmonotonic default logic are elements of ∆n+1 but not Σ n nor Π n for some n ≥1 in Kleene- Mostowski hierarchy of arithmetical sets.

3

Complexity of the Unique Extension Problem in Default Logic

Zhao X., Liberatore P.

Fundamenta Informaticae

|

2002

|

Vol. 53, nr 1

79-104

EN

In this paper we analyze the problem of checking whether a default theory has a single extension. This problem is important for at least three reasons. First, if a theory has a single extension, nonmonotonic inference can be reduced to entailment in propositional logic (which is computationally easier) using the set of consequences of the generating defaults. Second, a theory with many extensions is typically weak i.e., it has few consequences; this indicates that the theory is of little use, and that new information has to be added to it, either as new formulae, or as preferences over defaults. Third, some applications require as few extensions as possible (e.g. diagnosis). We study the complexity of checking whether a default theory has a single extension. We consider the combination of several restrictions of default logics: seminormal, normal, disjunction-free, unary, ordered. Complexity varies from the first to the third level of the polynomial hierarchy. The problem of checking whether a theory has a given number of extensions is also discussed.

4

Computation of extensions of seminormal default theories

Su K., Li W.

Fundamenta Informaticae

|

1999

|

Vol. 40, Nr 1

79-102

EN

In Reiter's default logic, the operator in the fixed-point definition of extension is not appropriate to compute extensions by its iterated applications. This paper presents a class of alternative operators, called compatible ones, such that, at least for normal default theories and so-called well-founded, ordered default theories, we can get extensions by iterated applications of them. In addition, we completely answer Etherington's conjectures about both his procedure for generating extensions and a modified version of it. In particular, we give an example of a finite, ordered default theory, for which the original procedure fails to converge, and show that the computation of the modified one is essentially the iteration of a compatible operator and converges for finite, ordered theories