Logic Programming And Nonmonotonic Reasoning

This paper presents an extension of disjunctive datalog (Data-log∨,⌝) by integrity constraints. In particular, besides classical integrity constraints (called strong constraints in this paper), the notion of weak constraints is introduced in the language. These are constraints that are satisfied if possible. The semantics of weak constraints tends to minimize the number of violated instances. As a consequence, weak constraints differ from strong constraints only if the latter are unsatisfiable. Weak constraints may be ordered according to their importance to express different priority levels. The formal definition of the semantics of weak constraints is given in a general way that allows to put them on top of any existing (model-theoretic) semantics for Datalog∨,⌝ programs. A number of examples shows that the proposed language (call it Data-log∨,⌝, c) is well-suited to represent complex knowledge-based problems, such as, for instance, NP optimization problems.A detailed complexity analysis of the language is given as well as an algorithm for the computation of the stable model semantics of Datalog∨,⌝c programs.

In this paper, we define and investigate the complexity of several nonmonotonic logics with quantified Boolean formulas as constraints. We give quantified constraint versions of the constraint programming formalism of Marek, Nerode, and Remmel [15] and of the natural extension of their theory to default logic. We also introduce a new formalism which adds constraints to circumscription. We show that standard complexity results for each of these formalisms generalize in the quantified constraint case. Gogic, Kautz, Papadimitriou, and Selman [8] have introduced a new method for measuring the strengths of reasoning formalisms based on succinctness of model representation. We show a natural hierarchy based on this measure exists between our versions of logic programming, circumscription, and default logic. Finally, we discuss some results about the relative succinctness of our reasoning formalisms versus any formalism for which model checking can be done somewhere in the polynomial time hierarchy.

We present a bottom-up algorithm for the computation of the well-founded model of non-disjunctive logic programs which is based on the set of elementary program transformations studied by Brass and Dix [4, 5]. The transformation approach has been introduced in more detail in [7]. In this paper we present a deeper analysis of its complexity and describe an optimized SCC-oriented evaluation. We show that by our method no more work is done than by the alternating fixpoint procedure [23, 24] and that there are examples where our algorithm is significantly superior.

Although it has been shown that non-monotonic reasoning is presumably harder than classical reasoning, there are cases where a non-monotonic treatment actually simplifies matters. Indeed, one of the reasons for considering non-monotonic systems is the hope of speeding up reasoning, and not to slow it down. In this paper, we consider proof lengths in a cut-free sequent calculus, and we show that the application of circumscription (or completion) to certain first-order formulae leads to a non-elementary speed-up of proof length. This is possible because the introduction of the completion formula can simulate the cut rule.

We study the computational properties of the prepositional fragment of Levesque's logic of only knowing. In particular, we show that the problem of reasoning with only knowing in the prepositional case lies at the second level of the polynomial hierarchy. Thus, it is as hard as reasoning in the majority of propositional formalisms for nonmonotonic reasoning, like default logic, circumscription and autoepistemic logic, and it is easier than reasoning in propositional formalisms based on the minimal knowledge paradigm, which is strictly related to the notion of only knowing.

Limiting the number of times a variable appears in either the head or the body of a rule, we identify two classes of normal prepositional logic programs. These classes have the desirable property that stable models, if they exist, can be found in linear time (worst case). We also identify a related class containing programs for which the well-founded model can be acquired in linear time, yet for which computing the stable model(s) remains NP-complete. We show in this class how, by relaxing one constraint, previously linear complexity is increased to intractability.

We present cellular automata on appropriate digraphs and show that any covered normal logic program is a cellular automaton. Seeing programs as cellular automata shifts attention from classes of Herbrand models to orbits of Herbrand interpretations. Orbits capture both the declarative, model-theoretic meaning of programs as well as their inferential behavior. Logically and intentionally different programs can produce orbits that simulate each other. Simple examples of such behavior are compellingly exhibited with space-time diagrams of the programs as cellular automata. Construing a program as a cellular automaton leads to a general method for simulating any covered program with a Horn clause program. This means that orbits of Horn programs are completely representative of orbits of covered normal programs.

This paper investigates separated autoepistemic logic which is a generalization of Moore's autoepistemic logic with separate modalities for belief and disbelief. Along the separation of beliefs and disbeliefs, the relationship between autoepistemic logic and default logic becomes very intuitive. Straightforward ways of translating default theories into separated autoepistemic theories and back are presented. These translations are shown to preserve a variety of semantics of default theories such as those based on default extensions, weak extensions and stationary extensions. These classes of extensions are captured by their analogs in separated autoepistemic logic, and vice versa. A particular novelty of the approach is that a reasonable notion of separated stationary expansions can be established.

We present a spectrum of default logics, using powerdomains to encode default constraints. The resulting nonmonotonic entailment relations all satisfy the law of reasoning by cases. This result is a consequence of two general theorems valid for any Scott domain: the Dichotomy Theorem and the Extension Splitting Theorem. We briefly indicate that for propositional logic, the complexity of entailment is complete for co-NP(3).

We represent Przymusinski's Autoepistemic Logic of Beliefs and the associated static semantics in terms of a general formalism of biconsequence relations suggested in [3]. It is shown, in particular, that the static semantics belongs to a broad family of nonmonotonic formalisms constructed in accordance with a common completion schema. We consider also a formal representation for two important special cases covering, respectively, belief theories without nested modalities and theories serving as translations of general logic programs. The representation of the latter will allow us to clarify a place of the static semantics for logic programs in the general classification proposed in [5].

An extension of resolution for skeptical stable model semantics is introduced. Unlike previous approaches, our calculus often needs to consider only a strict subset of the program rules. Moreover, we characterize a large class of programs whose derivations may proceed in a thoroughly goal-directed way. Some inferences, which depend on non-ground negative goals, can be drawn without resorting to negation-as-failure; as a consequence, many goals which flounder in the standard setting, have a successful skeptical derivation. The paper contains a preliminary study of some interesting derivation strategies.

Turi [20] introduced the important notion of a constrained atom: an atom with associated equality and disequality constraints on its arguments. A set of constrained atoms is a constrained interpretation. We show how non-ground representations of both the stable model and the well-founded semantics may be obtained through Turi's approach. As a practical consequence, the well-founded model (or the set of stable models) may be partially pre-computed at compile-time, resulting in the association of each predicate symbol in the program to a constrained atom. Algorithms to create such models are presented. Query processing reduces to checking whether each atom in the query is true in a stable model (resp. well-founded model). This amounts to showing the atom is an instance of one of some constrained atom whose associated constraint is solvable. Various related complexity results are explored, and the impacts of these results are discussed from the point of view of implementing systems that incorporate the stable and well-founded semantics.

In this talk, we will discuss the increasing need for integrated information services in industry. Dynamic forces are driving the need for increasing levels of integration among data sources in industry. These forces are an increasingly competitive marketplace, in which a company's ability to profit is directly related to its ability to access and use information, an increasing trend toward merging business units, which requires the integration of disparate information systems in order for the resulting business unit to achieve economies of scale, and finally, an increasing trend toward companies becoming less horizontally or vertically integrated, which requires that they partner with other companies to respond to market demands.

In an oversimplified and abstract view, given a logic (syntax, semantics, inference system) L and a knowledge base K of formulae in L.“computer” for K enables the user to provide an expression (term, formula, program) T with a free variable x and a value υ (from an appropriate domain) and “evaluates” T_x←υ (T with υ substituted for x) w.r.t. K in L.“solver” for K enables the user to provide an expression T with a free variable x and produces (all) values υ for which T_x←υ holds w.r.t. K in L, and“prover” for K enables the user to provide an expression T with a free variable x and generates a proof (or disproves) that, for all values υ, T_x←υ holds w.r.t. K in L.

We begin by motivating the use of paraconsistency and the detection of contradiction supported conclusions by recourse to examples. Next we overview WFSX_P and present its embedding into WFS. We then address the problem of detecting contradiction support and relate it to WFSX_p's intrinsic properties. Afterwards, we show how to implement two recent modal contradiction related constructs in the language of extended logic programs in order to gain explicit control of contradiction propagation. We finish by making comparisons and drawing some conclusions.

A new method is proposed of restoring integrity constraints after committing an external update of a data base. This method is conservative in the sense that it performs the minimum of the necessary changes in the initial data base. The method is based on a novel idea of a so called preference strategy, i.e. an “oracle” which resolves globally all the conflicts, taking into account the update to be committed.

A general framework for revision of nonmonotonic theories is presented. This framework can be applied if the intended nonmonotonic semantics is not (weakly) cumulative. For weaker semantics, it is shown that revision by contraction is not possible whenever the intended semantics satisfies Weak Cut and revision by expansion fails whenever Weak (Cautious) Monotony fails. Furthermore, it turns out that revision by expansion can be used to test whether the framework can be applied successfully and we analyse the case for logic programming.

The program composition approach can be fruitfully applied to combine general logic programs, i.e. logic programs possibly containing negative premises. We show how the introduction of a basic set of (meta-level) composition operations over general programs increases the knowledge representation capabilities of logic programming for non-monotonic reasoning. Examples of modular programming, hierarchical reasoning, constraints, and rules with exceptions will be illustrated. The semantics of programs and program compositions is defined in terms of three-valued logic [15]. The computational interpretation of program compositions is formalised by an equivalence preserving syntactic transformation of arbitrary program compositions into standard general programs.

The research on systems of logic programming with modules has followed two mainstreams, programming-in-the-large, where compositional operators are provided for combining separate and independent modules, and programming-in-the-small, which aims at enhancing logic programming with new logical connectives.In this paper, we present a general model theoretic approach to modular logic programming which combines programming in-the-large and in-the-small in a satisfactory way. Rather than inventing completely new constructs, however, we resort to a well-known concept in formal logic: generalized quantifiers. We show how generalized quantifiers can be incorporated into logic programs, both for Horn logic programs as well as in the presence of negation. Our basic observation is then that a logic program can be seen as a generalized quantifier, and we obtain a semantics for modular logic programs this way.Generalized quantifiers in logic programs gives rise to interesting classes of logic programs. We present a taxonomy of natural such classes, and investigate their properties. In particular, their expressive power over finite structures is analyzed.

We suggest to consider the class of logic programs with the new nonmonotonic operator which we call universally quantified embedded implication. By such implications we mean formulas of the form ∀x₁⋯∀x_l(P₁ & ⋯ & P_m → Q₁ & ⋯ & Q_n). The main subject of the paper is lifting notions and theorems, related to normal logic programs, to programs with universally quantified embedded implications. For this class of programs we define the standard model semantics for stratified programs, the stable model semantics, the well-founded semantics. We show that main properties of above semantics for normal logic programs hold as well for programs with implications. Besides, we investigate the possibilities of reducing programs with implications to normal logic programs. Finally we define a calculus corresponding to SLDNF-calculus [9] and prove theorem of its soundness.

Generalized queries are defined as sets of clauses in implicationform. They cover several tasks of practical importance for database maintenance such as answering positive queries, computing database completions and integrity constraints checking. We address the issue of nswering generalized queries under the minimal model semantics for the class of Disjunctive Deductive Databases (DDDBs). Our approach is based on having the query induce an order on the models returned by a sound and complete minimal model generating procedure. We consider answers that are true in all and those that are true in some minimal models of the theory and investigate the monotonicity properties of the different classes of queries and answers.

This paper gives a brief high-level description of the implementation of a disjunctive logic programming system referred to as DisLoP. This system is a result of research activities of the Disjunctive Logic Programming-project (funded by Deutsche Forschungs-Gemeinschaft), undertaken by the University of Koblenz since July 1995.

In this article we describe the non-monotonie reasoning system REVISE that revises contradictory extended logic programs. We sketch the REVISE algorithm and evaluate it in the domain of digital circuits.

Disjunctive Deductive Databases (DDDBs) — function-free disjunctive logic programs with negation in rule bodies allowed — have been recently recognized as a powerful tool for knowledge representation and commonsense reasoning. Much research has been spent on issues like semantics and complexity of DDDBs, but the important area of implementing DDDBs has been less addressed so far. However, a thorough investigation thereof is a basic requirement for building systems which render previous foundational work on DDDBs useful for practice.This paper presents the architecture of a DDDB system currently developed at TU Vienna in the FWF project P11580-MAT “A Query System for Disjunctive Deductive Databases”.

In this paper we present a new system for non-monotonic reasoning performed using abduction. The system, called ACLP, is a programming language based on the framework of Abductive and Constraint Logic Programming (ACLP) which integrates abduction and constraint solving in Logic Programming. It is build on top of the ECLiPSe language for Constraint Logic Programming (CLP) interfacing (and exploiting) appropriately the non-monotonic reasoning of abduction with the specialized constraint solving of the CLP language. ACLP is intended as a programming language that extends the underlying CLP language in which using NMR (in this case abduction) together with constraint solving it is possible to develop flexible solutions that are computationally viable in the real-life domain.We present the basic theory of ACLP that underlies the system, the main features of the ACLP language and how it can be used when developing applications. We then report on some experiments performed in order to test the cost of the use of the ACLP system as compared with the direct use of the (lower level) constraint solving framework of CLP on which this is build. These experiments provide evidence that the non-monotonic framework of ACLP does not compromise significantly the computational efficiency of the solutions thus confirming the computational viability of the framework for the development of flexible solutions to real-life applications.

The advantages of [[Florid]] as a deductive object-oriented database system are the rich object-oriented modeling facilities of its language F-logic. The focus of this paper is on [[Florid's]] multiple inheritance mechanism which turns out to be a useful means to adapt various examples of nonmonotonic reasoning in the object-oriented setting.

GLUE is a system to combine heterogeneous and distributed sources of information with a deductive kernel. For this purpose access methods for external sources of information, like databases, can be specified. Pieces of a program are generated from such a specification which can be used also in other programs. This technique has been developed with an application to theorem provers in mind. We will show how GLUE can be used either stand-alone or together with a theorem prover like PROTEIN to solve real world problems. Some examples of problems utilizing such a combination are presented.

The Smodels system is a C++ implementation of the well-founded and stable model semantics for range-restricted function-free normal programs. The system includes two modules: (i) smodels which implements the two semantics for ground programs and (ii) parse which computes a grounded version of a range-restricted function-free normal program. The latter module does not produce the whole set of ground instances of the program but a subset that is sufficient in the sense that no stable models are lost. The implementation of the stable model semantics for ground programs is based on bottom-up backtracking search where a powerful pruning method is employed. The pruning method exploits an approximation technique for stable models which is closely related to the well-founded semantics. One of the advantages of this novel technique is that it can be implemented to work in linear space. This makes it possible to apply the stable model semantics also in areas where resulting programs are highly non-stratified and can possess a large number of stable models. The implementation has been tested extensively and compared with a state of the art implementation of the stable model semantics, the SLG system. In tests involving ground programs it clearly outperforms SLG.

The well-founded model provides a natural and robust semantics for logic programs with negative literals in rule bodies. We implemented the well-founded semantics in the SLG-WAM of XSB [19]. Performance results indicate that the overhead of delay and simplification to Prolog — or tabled — evaluations is minimal. To compute the well-founded semantics, the SLG-WAM adds to an efficient tabling engine for definite programs three operations — negative loop detection, delay and simplification — which serve to detect, to break and to resolve cycles through negation that might arise in evaluating normal programs. XSB is a full Prolog system that closely approximates the ISO standard; additionally, it supports a tight integration of tabled predicates with nontabled predicates.

We present an implementation platform for query-answering in default logics. The overall approach along with its implementation, the XRay system, allows for query-answering from default theories supporting local proof procedures. The deductive power of XRay stems from it susage of Prolog Technology Theorem Proving Techniques (PTTP) supported by further enhancements, such as default lemma handling and regularity-based truncations of the underlying search space. The generality of the approach, allowing for a (simultaneous) treatment of different default logics, stems from a novel model-based approach to consistency checking.