Catálogo de publicaciones - libros

The paper presents DLV a Disjunctive Logic Programming system with object-oriented constructs, including classes, objects, (multiple) inheritance, and types. DLV is built on top of DLV (a state-of-the art DLP system), and provides a graphical user interface that allows to specify, update, browse, query, and reason on knowledge bases. Two strong points of the system are the powerful type-checking mechanism, and the advanced interface for visual querying.

In this work we describe a system for determining of disjunctive datalog programs under the stable model semantics. The problem is tackled by reducing it to the unsatisfiability problem of first-order formulas in the Bernays-Schönfinkel fragment. We then employ a tableaux-based theorem prover, which (unlike most other currently available provers) is guaranteed to terminate for these formulas. To the best of our knowledge, this is the first strong equivalence tester for disjunctive non-ground datalog.

This paper describes a system called for studying strong equivalence in answer set logic programming. The basic function of the system is to check if two given ground disjunctive logic programs are equivalent, and if not, return a counter-example. We have used the system to discover some interesting theorems about strong equivalence [Lin and Chen, 2005]. Here we briefly describe how the system can be used to find out whether a given set of rules is strongly equivalent to another, perhaps simpler set of rules.

Disjunctive logic programming under the stable model semantics [GL91] is a new methodology called (ASP) for solving combinatorial search problems. This programming method uses answer set solvers, such as [Lea05], [Jea05], [SS05], [LZ02], [Lie05a]. Systems and are more general as they work with the class of disjunctive logic programs, while other systems cover only normal programs. DLV is uniquely designed to find the answer sets for disjunctive logic programs. On the other hand, first generates possible stable model candidates and then tests the candidate on the minimality using system SMODELS as an inference engine for both tasks. Systems CMODELS and ASSAT use SAT solvers as search engines. They are based on the relationship between the completion semantics [Cla78], loop formulas [LZ02] and answer set semantics for logic programs. Here we present the implementation of a SAT-based algorithm for finding answer sets for disjunctive logic programs within . The work is based on the definition of completion for disjunctive programs [LL03] and the generalisation of loop formulas [LZ02] to the case of disjunctive programs [LL03]. We propose the necessary modifications to the SAT based ASSAT algorithm [LZ02] as well as to the generate and test algorithm from [GLM04] in order to adapt them to the case of disjunctive programs. We implement the algorithms in and demonstrate the experimental results.