Logic Programming and Nonmonotonic Reasoning

FLORA-2 is an advanced knowledge representation system that integrates F-logic, HiLog, and Transaction Logic. In this paper we give an overview of the theoretical foundations of the system and of some of the aspects of nonmonotonic reasoning in FLORA-2. These include scoped default negation, behavioral inheritance, and nonmonotonicity that stems from database dynamics.

The rapid expansion of the Internet and World Wide Web led to growing interest in data and information integration, which should be capable to deal with inconsistent and incomplete data. Answer Set solvers have been considered as a tool for data integration systems by different authors. We discuss why data integration can be an interesting model application of Answer Set programming, reviewing valuable features of non-monotonic logic programs in this respect, and emphasizing the role of the application for driving research.

Project Halo is a multi-staged effort, sponsored by Vulcan Inc, aimed at creating the Digital Aristotle (DA), an application that will encompass much of the world’s scientific knowledge and be capable of applying sophisticated problem solving to answer novel questions. Vulcan envisions two primary roles for the Digital Aristotle: as a tutor to instruct students in the sciences, and as an interdisciplinary research assistant to help scientists in their work. As a first step towards this goal, there was a six-month Pilot phase, designed to assess the state of the art in applied Knowledge Representation and Reasoning (KR&R). Vulcan selected three teams, each of which was to formally represent 70 pages from the Advanced Placement (AP) chemistry syllabus and deliver knowledge based systems capable of answering questions on that syllabus. The evaluation quantified each system’s

coverage

of the syllabus in terms of its ability to answer novel, previously unseen questions and to provide

human-readable

answer justifications. These justifications will play a critical role in building user trust in the question-answering capabilities of the Digital Aristotle.Despite differences in approach, all three systems did very well on the challenge, achieving performance comparable to the human median. The analysis also provided key insights into how the approaches might be scaled, while at the same time suggesting how the cost of producing such systems might be reduced.

Aggregates in answer set programming (ASP) have recently been studied quite intensively. The main focus of previous work has been on defining suitable semantics for programs with arbitrary, potentially recursive aggregates. By now, these efforts appear to have converged. On another line of research, the relation between unfounded sets and (aggregate-free) answer sets has lately been rediscovered. It turned out that most of the currently available answer set solvers rely on this or closely related results (e.g., loop formulas).

In this paper, we unite these lines and give a new definition of unfounded sets for disjunctive logic programs with arbitrary, possibly recursive aggregates. While being syntactically somewhat different, we can show that this definition properly generalizes all main notions of unfounded sets that have previously been defined for fragments of the language.

We demonstrate that, as for restricted languages, answer sets can be crisply characterized by unfounded sets: They are precisely the unfounded-free models. This result can be seen as a confirmation of the robustness of the definition of answer sets for arbitrary aggregates. We also provide a comprehensive complexity analysis for unfounded sets, and study its impact on answer set computation.

Loops and the corresponding loop formulas play an important role in answer set programming. On the one hand, they are used for guaranteeing correctness and completeness in SAT-based answer set solvers. On the other hand, they can be used by conventional answer set solvers for finding unfounded sets of atoms. Unfortunately, the number of loops is exponential in the worst case. We demonstrate that not all loops are actually needed for answer set computation. Rather, we characterize the subclass of

elementary loops

and show that they are sufficient and necessary for selecting answer sets among the models of a program’s completion. Given that elementary loops cannot be distinguished from general ones in atom dependency graphs, we show how the richer graph structure provided by

body-head dependency graphs

can be exploited for this purpose.

We investigate techniques for approximating answer sets of general logic programs of Lifschitz and Woo, whose rules have single literals as heads. We propose three different methods of approximation and obtain results on the relationship between them. Since general logic programs with single literals as heads are equivalent to revision programs, we obtain results on approximations of justified revisions of databases by revision programs.

Given two classes of logic programs, we may be interested in modular translations from one class into the other that are sound with respect to the answer set semantics. The main theorem of this paper characterizes the existence of such a translation in terms of strong equivalence. The theorem is used to study the expressiveness of several classes of programs, including the comparison of cardinality constraints with monotone cardinality atoms.

Open answer set programming (OASP) is an extension of answer set programming where one may ground a program with an arbitrary superset of the program’s constants. We define a fixed point logic (FPL) extension of Clark’s completion such that open answer sets correspond to models of FPL formulas and identify a syntactic subclass of programs, called (loosely) guarded programs. Whereas reasoning with general programs in OASP is undecidable, the FPL translation of (loosely) guarded programs falls in the decidable (loosely) guarded fixed point logic (

μ

(L)GF).

Moreover, we reduce normal closed ASP to loosely guarded OASP, enabling a characterization of an answer set semantics by

μ

LGF formulas. Finally, we relate guarded OASP to Datalog LITE, thus linking an answer set semantics to a semantics based on fixed point models of extended stratified Datalog programs. From this correspondence, we deduce 2-EXPTIME-completeness of satisfiability checking w.r.t. (loosely) guarded programs.

The paper introduces Answer Set Programming with External Predicates (

ASP-EX

), a framework aimed at enabling ASP to deal with external sources of computation. This feature is realized by the introduction of “parametric”

external predicates

, whose extension is not specified by means of a logic program but computed through external code. With respect to existing approaches it is explicitly addressed the issue of invention of new information coming from external predicates, in form of new, and possibly infinite, constant symbols. Several decidable restrictions of the language are identified as well as suitable algorithms for evaluating Answer Set Programs with external predicates. The framework paves the way to Answer Set Programming in several directions such as pattern manipulation applications, as well as the possibility to exploit function symbols.

ASP-EX

has been successfully implemented in the

DLV

system, which is now enabled to make external program calls.

Equilibrium logic, introduced by David Pearce, extends the concept of an answer set from logic programs to arbitrary sets of formulas. Logic programs correspond to the special case in which every formula is a “rule” — an implication that has no implications in the antecedent (body) and consequent (head). The semantics of equilibrium logic looks very different from the usual definitions of an answer set in logic programming, as it is based on Kripke models. In this paper we propose a new definition of equilibrium logic which uses the concept of a reduct, as in the standard definition of an answer set. Second, we apply the generalized concept of an answer set to the problem of defining the semantics of aggregates in answer set programming. We propose, in particular, a semantics for weight constraints that covers the problematic case of negative weights. Our semantics of aggregates is an extension of the approach due to Faber, Leone, and Pfeifer to a language with choice rules and, more generally, arbitrary rules with nested expressions.

We introduce a declarative approach for a coherent composition of autonomous databases. For this we use ID-logic, a formalism that extends classical logic with inductive definitions. We consider ID-logic theories that express, at the same time, the two basic challenges in database composition problems: relating different schemas of the local databases to one global schema (

schema integration

) and amalgamating the distributed and possibly contradictory data to one consistent database (

data integration

). We show that our framework supports different methods for schema integration (as well as their combinations) and that it provides a straightforward way of dealing with inconsistent data. Moreover, this framework facilitates the implementation of database repair and consistent query answering by means of a variety of reasoning systems.

The

Closed-World Assumption

(CWA) on a database expresses that an atom not in the database is false. The CWA is only applicable in domains where the database has complete knowledge. In many cases, for example in the context of distributed databases, a data source has only complete knowledge about part of the domain of discourse. In this paper, we introduce an expressive and intuitively appealing method of representing a

local closed-world assumption

(LCWA) of autonomous data-sources. This approach distinguishes between the data that is conveyed by a data-source and the meta-knowledge about the area in which these data is complete. The data is stored in a relational database that can be queried in the standard way, whereas the meta-knowledge about its completeness is expressed by a first order theory that can be processed by an independent reasoning system (for example a

mediator

). We consider different ways of representing our approach, relate it to other methods of representing local closed-word assumptions of data-sources, and show some useful properties of our framework which facilitate its application in real-life systems.

Possibilistic Defeasible Logic Programming (P-DeLP) is a logic programming language which combines features from argumentation theory and logic programming, incorporating as well the treatment of possibilistic uncertainty and fuzzy knowledge at object-language level. Solving a P-DeLP query

Q

accounts for performing an exhaustive analysis of arguments and defeaters for

Q

, resulting in a so-called dialectical tree, usually computed in a depth-first fashion. Computing dialectical trees efficiently in P-DeLP is an important issue, as some dialectical trees may be computationally more expensive than others which lead to equivalent results. In this paper we explore different aspects concerning how to speed up dialectical inference in P-DeLP. We introduce definitions which allow to characterize dialectical trees constructively rather than declaratively, identifying relevant features for pruning the associated search space. The resulting approach can be easily generalized to be applied in other argumentation frameworks based in logic programming.

In this paper we generalize the notion of approximation of action theories introduced in [13,26]. We introduce a logic programming based method for constructing approximation of action theories of

$\mathcal{AL}$

and prove its soundness. We describe an approximation based conformant planner and compare its performance with other state-of-the-art conformant planners.

We present the action language

$\mathcal{GC}+$

for reasoning about actions in multi-agent systems under probabilistic uncertainty and partial observability, which is an extension of the action language

$\mathcal{C}+$

that is inspired by partially observable stochastic games (POSGs). We provide a finite-horizon value iteration for this framework and show that it characterizes finite-horizon Nash equilibria. We also describe how the framework can be implemented on top of nonmonotonic causal theories. We then present acyclic action descriptions in

$\mathcal{GC}+$

as a special case where transitions are computable in polynomial time. We also give an example that shows the usefulness of our approach in practice.

The formalism of nonmonotonic causal theories (Giunchiglia, Lee, Lifschitz, McCain, Turner, 2004) provides a general-purpose formalism for nonmonotonic reasoning and knowledge representation, as well as a higher level, special-purpose notation, the action language

$\mathcal{C}+$

, for specifying and reasoning about the effects of actions and the persistence (‘inertia’) of facts over time. In this paper we investigate some logical properties of these formalisms. There are two motivations. From the technical point of view, we seek to gain additional insights into the properties of the languages when viewed as a species of conditional logic. From the practical point of view, we are seeking to find conditions under which two different causal theories, or two different action descriptions in

$\mathcal{C}+$

, can be said to be equivalent, with the further aim of helping to decide between alternative formulations when constructing practical applications.

We describe

$\mathcal{M}$

odular-

ε

(

$\mathcal{ME}$

), a specialized, model-theoretic logic for narrative reasoning about actions, able to represent non-deterministic domains involving concurrency, static laws (constraints) and indirect effects (ramifications). We give formal results which characterize

$\mathcal{ME}$

’s high degree of modularity and elaboration tolerance, and show how these properties help to separate out, and provide a principled solutions to, the endogenous and exogenous qualification problems. We also show how a notion of (micro) processes can be used to facilitate reasoning at the dual levels of temporal granularity necessary for narrative-based domains involving “instantaneous” series of indirect and knock-on effects.

We propose a model to manage the distributed computation of answer sets within a general framework. This design incorporates a variety of software and hardware architectures and allows its easy use with a diverse cadre of computational elements. Starting from a generic algorithmic scheme, we develop a platform for distributed answer set computation, describe its current state of implementation, and give some experimental results.

Recent research on answer set programming (ASP) systems, has mainly focused on solving NP problems more efficiently. Yet, disjunctive logic programs allow for expressing every problem in the complexity classes

$\Sigma^P_2$

and

$\Pi^P_2$

. These classes are widely believed to be strictly larger than NP, and several important AI problems, like conformant and conditional planning, diagnosis and more are located in this class.

In this paper we focus on improving the evaluation of

$\Sigma^P_2$

/

$\Pi^P_2$

-hard ASP programs. To this end, we define a new heuristic

h

DS

and implement it in the (disjunctive) ASP system DLV. The definition of

h

DS

is geared towards the peculiarites of hard programs, while it maintains the benign behaviour of the well-assessed heuristic of DLV for NP problems.

We have conducted extensive experiments with the new heuristic.

h

DS

significantly outperforms the previous heuristic of DLV on hard 2QBF problems. We also compare the DLV system (with

h

DS

) to the QBF solvers SSolve, Quantor, Semprop, and yQuaffle, which performed best in the QBF evaluation of 2004. The results of the comparison indicate that ASP systems currently seem to be the best choice for solving

$\Sigma^P_2$

/

$\Pi^P_2$

-complete problems.

Goal-directed fixed point computation strategies have been widely adopted in the tabled logic programming paradigm. However, there are many situations in which a fixed point contains a large number or even infinite number of solutions. In these cases, a fixed point computation engine may not be efficient enough or feasible at all. We present a mode-declaration scheme which provides the capabilities to reduce a fixed point from a big solution set to a preferred small one, or from an infeasible infinite set to a finite one. We show the correctness of the mode-declaration scheme. One motivating application of our mode-declaration scheme is for dynamic programming, which is typically used for solving optimization problems. There is no need to define the value of an optimal solution recursively, instead, defining a general solution suffices. The optimal value as well as its corresponding concrete solution can be derived implicitly and automatically using a mode-directed fixed point computation engine. This mode-directed fixed point computation engine has been successfully implemented in a commercial Prolog system.

In answer set programming systems like Smodels and some SAT solvers, constraint propagation is carried out by a mechanism called lookahead. The question arises as what is the pruning power of lookahead, and how such pruning power fares in comparison with the consistency techniques in solving CSPs. In this paper, we study the pruning power of lookahead by relating it to local consistencies under two different encodings from CSPs to answer set programs. This leads to an understanding of how the search space is pruned in an answer set solver with lookahead for solving CSPs. On the other hand, lookahead as a general constraint propagation mechanism provides a uniform algorithm for enforcing a variety of local consistencies. We also study the impact on the search efficiency under these encodings.

Nested logic programs and epistemic logic programs are two important extensions of answer set programming. However, the relationship between these two formalisms is rarely explored. In this paper we first introduce the epistemic HT-logic, and then propose a more general extension of logic programs called

nested epistemic logic programs

. The semantics of this extension – named

equilibrium views

– is defined on the basis of the epistemic HT-logic. We prove that equilibrium view semantics extends both the answer sets of nested logic programs and the world views of epistemic logic programs. Therefore, our work establishes a unifying framework for both nested logic programs and epistemic logic programs. Furthermore, we also provide a characterization of the strong equivalence of two nested epistemic logic programs.

ID-logic uses ideas from the field of logic programming to extend second order logic with non-monotone inductive defintions. In this work, we reformulate the semantics of this logic in terms of approximation theory, an algebraic theory which generalizes the semantics of several non-monotonic reasoning formalisms. This allows us to apply certain abstract modularity theorems, developed within the framework of approximation theory, to ID-logic. As such, we are able to offer elegant and simple proofs of generalizations of known theorems, as well as some new results.

The main construction in this paper is an encoding of default logic into an “only knowing” logic with degrees of confidence. By imposing simple and natural constraints on the encoding we show that the “only knowing” logic can accommodate ordered default theories and that the constrained encoding implements a prescriptive interpretation of preference between defaults. An advantage of the encoding is that it provides a transparent formal rendition of such a semantics. A feature of the construction is that the generation of extensions can be carried out within the “only knowing” logic, using object level concepts alone.

As in human world many of our goals could not be achieved without interacting with other people, in case many agents are part of the same environment one agent should be aware that he is not alone and he cannot assume other agents sharing his own goals. Moreover, he may be required to interact with other agents and to reason about their mental state in order to find out potential friends to join with (or opponents to fight against). In this paper we focus on a language derived from logic programming which both supports the representation of mental states of agent communities and provides each agent with the capability of reasoning about other agents’ mental states and acting accordingly. The proposed semantics is shown to be translatable into stable model semantics of logic programs with aggregates.

Two approaches to logic programming with probabilities emerged over time: bayesian reasoning and probabilistic satisfiability (PSAT). The attractiveness of the former is in tying the logic programming research to the body of work on Bayes networks. The second approach ties computationally reasoning about probabilities with linear programming, and allows for natural expression of imprecision in probabilities via the use of intervals.

In this paper we construct precise semantics for one PSAT-based formalism for reasoning with inteval probabilities, probabilistic logic programs (p-programs), orignally considered by Ng and Subrahmanian. We show that the probability ranges of atoms and formulas in p-programs cannot be expressed as single intervals. We construct the prescise description of the set of models of p-programs and study the computational complexity if this problem, as well as the problem of consistency of a p-program. We also study the conditions under which our semantics coincides with the single-interval semantics originally proposed by Ng and Subrahmanian for p-programs. Our work sheds light on the complexity of construction of reasoning formalisms for imprecise probabilities and suggests that interval probabilities alone are inadequate to support such reasoning.

We present an alternative model theory for answer sets based on the possible worlds semantics proposed by Routley (1974) as a framework for the propositional logics of Fitch and Nelson. By introducing a falsity constant or second negation into Routley models, we show how paraconsistent as well as ordinary answer sets can be represented via a simple minimality condition on models. This means we can define a paraconsistent version of equilibrium logic, or paraconsistent answer sets (PAS) for propositional theories. The underlying logic of PAS is denoted by

N

9

. We characterise it axiomatically and algebraically, showing it to be the least conservative extension of the logic of here-and-there with strong negation. In addition, we show that

N

9

captures the strong equivalence of programs in the paraconsistent case and can thus serve as a useful mathematical foundation for PAS. We end by showing that

N

9

has the Interpolation Property.

Multidimensional dynamic logic programs

are a paradigm which allows to express (partially) hierarchically ordered evolving knowledge bases through (partially) ordered multi sets of logic programs and allowing to solve contradictions among rules in different programs by allowing rules in more important programs to reject rules in less important ones. This class of programs extends the class of

dynamic logic program

that provides meaning and semantics to

sequences of logic programs

. Recently a semantics named

refined stable model semantics

has fixed some counterintuitive behaviour of previously existing semantics for dynamic logic programs. However, it is not possible to directly extend the definitions and concepts of the refined semantics to the multidimensional case and hence more sophisticated principles and techniques are in order. In this paper we face the problem of defining a proper semantics for multidimensional dynamic logic programs by extending the idea of well supported model to this class of programs and by showing that this concept alone is enough for univocally characterizing a proper semantics. We then show how the newly defined semantics coincides with the refined one when applied to sequences of programs.

Evolution is an important sub-area of study in biological science, where given a set of taxa, the goal is to reconstruct their evolutionary history, or phylogeny. One very recent approach is to predict a local phylogeny for every subset of 4 taxa, called a quartet topology, and then to assemble a phylogeny for the whole set of taxa satisfying these predicted quartet topologies. In general, the predicted quartet topologies might not always agree with each other, and thus the objective function becomes to satisfy a maximum number of them. This is the well known Maximum Quartet Consistency (MQC) problem. In the past, the MQC problem has been solved by dynamic programming and the so-called fixed-parameter method. Recently, we have proposed to solve the MQC in answer set programming. In this note, we summarize the theoretical results of this approach and report new experimental results for the purpose of comparison, which show that our approach in answer set programming is favored over the existing approaches based on dynamic programming and fixed-parameter method. In particular, some of the hard instances (where the error ratio is high) that were not reported to be solved in other approaches can now be solved in our approach.

ACMI is a decision support system for the checking of medical invoices in a German health insurance company. We present a brief overview of the system and its implementation in DLV.

The paper presents INFOMIX a successful application of ASP technology to the domain of Data Integration. INFOMIX is a novel system which supports powerful information integration, utilizing the ASP system DLV. While INFOMIX is based on solid theoretical foundations, it is a user-friendly system, endowed with graphical user interfaces for the average database user and administrator, respectively. The main features of the INFOMIX system are: (i) a comprehensive information model, through which the knowledge about the integration domain can be declaratively specified, (ii) capability of dealing with data that may result incomplete and/or inconsistent with respect to global constraints, (iii) advanced information integration algorithms, which reduce (in a sound and complete way) query answering to cautious reasoning on disjunctive Datalog programs, (iv) sophisticated optimization techniques guaranteeing the effectiveness of query evaluation in INFOMIX, (v) a rich data acquisition and transformation framework for accessing heterogeneous data in many formats including relational, XML, and HTML data.

We associate optimality theory with abduction and preference handling. We present linguistic problems that appear in the study of dialects as new application of abduction and preference handling. Differences in German dialects originate from different rankings of linguistic constraints which determine the well-formedness of expressions within a language. We introduce a framework for analyzing differences in German dialects by abduction of preferences. More precisely, we will take the perspective of a linguist and reconstruct dialectal variation as abduction problem: Given an observation that a sentence is found as grammatically correct, abduct the underlying constraint ranking. For this, we give a new definition for the determination of optimal candidates for total orders with indifferences. Additionally, we give an encoding for the diagnosis front-end of the

DLV

system.

We describe an application of Abductive Logic Programming (ALP) to the analysis of an important class of DNA microarray experiments. We develop an ALP theory that provides a simple and general model of how gene interactions can cause changes in observable expression levels of genes. Input to the procedure are the observed microarray results; output are hypotheses about possible gene interactions that explain the observed effects. We apply and evaluate our approach on microarray experiments on

M. tuberculosis

and

S. cerevisiae

.

The integration of preferences into Answer Set Programming (ASP) constitutes an important practical device for distinguishing certain preferred answer sets from non-preferred ones. Up to now, the preference semantics we are considering in this system description were incorporated into answer set solvers either by meta-interpretation [3] or by pre-compilation front-ends [2]; therefore, such kinds of preferences were never integrated into the core existing ASP solvers.

A number of answer set solvers have been proposed in recent years, such as

Smodels

, DLV, Cmodels, and ASSAT. Most existing ASP solvers have been extended to provide front-ends that are suitable to encode specialized forms of knowledge-e.g., weight-constraints, restricted forms of optimization, front-ends for planning and diagnosis. These features allow declarative solutions in speci.c application domains. However, this is not completely satisfactory:

– The development of an ASP program is viewed as a “monolithic” process. Most ASP systems offer only a batch approach to execution of programs-programs are completely developed, “compiled”, executed, and finally answer sets are proposed to the user. The process lacks any levels of interaction with the user. In particular, it does not directly support an interactive development of programs (as in Prolog), where one can immediately explore the results of simply adding/removing rules.

– ASP programmers can control the computation of answer sets through the rules that they include in the logic program. Nevertheless, ASP systems offer very limited capabilities for reasoning on the

whole class

of answer sets associated to a program-e.g., to perform selection of models according to user-defined criteria or to compare models. These activities are important in many application domains-e.g., to express soft constraints, to support preferences when using ASP to perform planning.

– ASP solvers are independent systems; interaction with other languages can be performed only through complex, low level APIs; this prevents programmers from writing programs that manipulate ASP programs and answer sets as first-class citizens. E.g., we wish to write programs in a high-level language (Prolog in this case), which are capable to access ASP programs, modify their structure (by adding or removing rules), and access and reason with answer sets. This type of features is essential in many domains-e.g., automatically modify the plan length in a planning problem.

The

stable model semantics

of disjunctive logic programs (DLPs) is based on minimal models [5,12] which makes atoms appearing in a disjunctive program false by default. This is often desirable from the knowledge representation point of view, but certain domains become awkward to formalize if all atoms are blindly subject to minimization. In contrast to this,

parallel circumscription

[11] provides a re.ned notion of minimal models as it distinguishes

varying

and

fixed

atoms in addition to those being falsified. This eases the task of knowledge presentation in many cases. For example, it is straightforward to formalize Reiter-style

minimal diagnoses

[13] for digital circuits using parallel circumscription.

We describe a new software,

pbmodels

, that uses pseudo-boolean constraint solvers (

PB

solvers) to compute stable models of logic programs with weight atoms. To this end,

pbmodels

converts ground logic programs to propositional theories with weight atoms so that stable models correspond to models. Our approach is similar to that used by

assat

and

cmodels

. However, unlike these two systems,

pbmodels

does not compile the weight atoms away. Preliminary experimental results on the performance of

pbmodels

are promising.

We present a monitoring tool for plan execution in non-deterministic environments, which are described in an action language, based on non-monotonic logic programming. Thanks to it, deviations of concrete executions from expected ones can be detected, and diagnostic explanations in terms of unsuccessful action executions can be obtained. The latter may be exploited for execution recovery, and may help in rectifying an incoherent view of the planning domain.

We present a new answer set solver

nomore

++. Distinguishing features include its treatment of heads and bodies equitably as computational objects and a new hybrid lookahead.

nomore

++ is close to being competitive with state-of-the-art answer set solvers, as demonstrated by selected experimental results.

In [2], we presented a system called

$\mathbb{ASP}$

-

$\mathbb{CLP}$

for computing answer sets of logic programs with aggregates. The implementation of

$\mathbb{ASP}$

-

$\mathbb{CLP}$

relies on the use of an external constraint solver (ECLiPSe) to deal with aggregate literals and requires some modifications to the answer set solver used in the experiment (

Smodels

). In general, the system is capable of computing answer sets of arbitrary programs with aggregates, i.e., there is no syntactical restrictions imposed on the inputs to the system. This makes

$\mathbb{ASP}$

-

$\mathbb{CLP}$

different from

dlv

A

(built BEN/5/23/04) [1], which deals with stratified programs only.

$\mathbb{ASP}$

-

$\mathbb{CLP}$

, however, is based on a semantics that does not guarantee minimality of answer sets. Furthermore, our experiments with

$\mathbb{ASP}$

-

$\mathbb{CLP}$

indicate that the cost of communication between the constraint solver and the answer set solver proves to be significant in large instances.

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

strong equivalence

of disjunctive

non-ground

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

SELP

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

answer set programming

(ASP) for solving combinatorial search problems. This programming method uses answer set solvers, such as

dlv

[Lea05],

gnt

[Jea05],

smodels

[SS05],

assat

[LZ02],

cmodels

[Lie05a]. Systems

dlv

and

gnt

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,

gnt

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

cmodels

. 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

cmodels

and demonstrate the experimental results.