Dagstuhl Seminar Report 9627

Following is the abstracts of the talks given at the Dagstuhl seminar 9627 on Disjunctive Logic Programming and Databases: Non-Monotonic Aspects.

Jump to names starting with: A * B * C * D * E * F * H * L * M * N * P * R * S * T * Y

José J. Alferes <jja@uevora.pt>

Departamento de Mathemática
Universidade de Évora
P-7000 Évora

Title: A non-monotonic logic program semantics and its implementation

Miscellaneous information: See the entry for Luís Moniz Pereira

Chandrabose Aravindan <arvind@informatik.uni-koblenz.de>

Fachbereich Informatik
Universität Koblenz-Landau
Rheinau 1
Koblenz D-56075
Tel: +49-261-9119 443
Fax: +49-261-9119 496

Title: Abduction and negation in disjunctive logic programming

Abstract: In this talk, we presented an abductive framework for disjunctive logic programming that captures the semantics of negation in disjunctive programs. Based on this framework, a new inference rule for negation, referred to as negation by failure to explain, was introduced for positive programs. This view of negation was shown to be equivalent to the semantics provided by (Extended) Generalized Closed World Assumption. This relationship between abduction and negation provides a clear methodology to develop algorithms for minimal model reasoning. To demonstrate this, we showed how a theorem prover based on restart model elimination calculus can be modified for abductive reasoning and thus for minimal model reasoning.

This report is available on-line as http://www.uni-koblenz.de/local/fb4/publications/GelbeReihe/RR-9-96.ps.gz

Chitta Baral <chitta@cs.utep.edu>

Department of Computer Science
University of Texas at El Paso
El Paso, Texas 79968, U.S.A.

Title: A Calculus for Disjunctive Logic Programs

Abstract: Proof procedures for logic programs are complex and usually defined in terms of complicated structures like trees (refer for example to SLDNF or SLINF trees). We would like to define a calculus for disjunctive logic programs similar to the SLDNF calculus introduced by Lifschitz for logic programs without disjunctions. As in the case of SLDNF we believe that this calculus will be significantly much simpler than the current proof procedures for disjunctive programs and will allow us to separate the questions on the procedures from the questions on the proofs. In the presentation we reviewed our initial investigation on the development of this calculus.

Miscellaneous information: Joint work with Jorge Lobo

Peter Baumgartner < peter@informatik.uni-koblenz.de>

University of Koblenz
Institute for Computer Science
Rheinau 1
Koblenz D-56075
Tel: +49-261-9119 426
Fax: +49-261-9119 496

Title: Hyper Tableaux. Part 1: Proof Procedure and Model Generation

Abstract: This paper introduces a variant of clausal normal form tableaux that we call "hyper tableaux". Hyper tableaux keep many desirable features of analytic tableaux while taking advantage of the central idea from (positive) hyper resolution, namely to resolve away all negative literals of a clause in a single inference step. Another feature of the proposed calculus is the extensive use of universally quantified variables. This enables new efficient forward-chaining proof procedures for full first order theories as variants of tableaux calculi.

This report is available on-line as http://www.uni-koblenz.de/universitaet/fb/fb4/publications/GelbeReihe/RR-8-96.ps.gz

Alexander Bochman < bochman@bimacs.cs.biu.ac.il>

Rh. Kiryat Sefer 18/12
Rishon Le-Zion 75220


Abstract: We suggest a general logical formalism for Logic Programming (called biconsequence relations) based on a four-valued inference. We show that it forms a proper setting for representing logic programs of a most general kind and for describing logics and semantics that characterize their behavior. In this way we also extend the connection between Logic and Logic Programming beyond positive programs.

A uniform representation of various semantics for logic programs is presented. The main conclusion from this representation is that the distinction between these semantics can be largely attributed to the difference in their underlying (monotonic) logical systems. Moreover, in most cases the difference can even be reduced to that of the language, that is, to the difference in the logical connectives allowed for representing derivable information. In addition, it allows us to see a reasoning about logic programs as a most simple kind of nonmonotonic reasoning in general.

Stefan Brass < sb@informatik.uni-hannover.de>

Universität Hannover
Institut für Informatik
Lange Laube 22
D-30175 Hannover
Phone: +49 511 762 4953
Fax:   +49 511 762 4961

Title: Modeltheoretic Characterization and Computation of the Static Semantics

Abstract: (Joint work with Jürgen Dix and Teodor C. Przymusinski.)

The autoepistemic logic of beliefs (AEB) extends propositional logic by a modal operator B for "is believed". The static semantics proposed by Przumusinski interprets B(F) as "F is true in all minimal models" (minimal with a fixed interpretation of the belief literals). Then not(F) is interpreted as a shorthand for B(~F).

We give a fixpoint construction for computing the models of the least static expansion for a class of theories which extends the class of disjunctive logic programs. The algorithm works by computing the minimal models and then iteratively eliminating those which are based on belief interpretations that cannot be represented as the "intersection" of some set of minimal models. The construction is based on a model-theoretic characterization via Kripke-structures.

This report is available on-line as ftp://ftp.informatik.uni-hannover.de/papers/1996/BDP96a.ps.gz

Miscellaneous information: A simple prototype implementation is available from ftp://ftp.informatik.uni-hannover.de/software/static/static.html.

Gerhard Brewka < brewka@informatik.uni-leipzig.de>

Institut für Informatik
Universität Leipzig
Augustusplatz 10-11
D-04109 Leipzig

Title: Well-Founded Semantics for Default Logic

Abstract: Default logic is one of the most popular approaches to model defeasible reasoning. Nevertheless, there are a number of problems with Reiter's original semantics that have led to the investigation of alternative approaches. In particular, Baral/Subrahmanian and Przymusinska/Przymusinski have investigated generalizations of well-founded semantics for normal logic programs to default logic.

These generalizations have a number of interesting properties. Unfortunately, it turns out that in many realistic situations they are unable to draw any defeasible conclusions at all - which can hardly be viewed as satisfactory. We show how this difficulty can be solved by varying the fixed point operator underlying the semantics. We define a range of different semantics. All of them are correct wrt. safe conclusions under Reiter's semantics, i.e. those conclusions with the same proof in all extensions. For the strongest semantics we have also completeness in the case of coherent default theories, i.e. default theories with at least one extension. The logics differ in the effort spent for determining potential conclusions.

We show that our approach also leads to new semantics for normal and extended logic programs. Moreover, we define prioritized versions of the logics.

Francois Bry < bry@informatik.uni-muenchen.de>

Computer Science Institute
Ludwig-Maximilians-Universität München
Oettingenstr. 67
80538 München, Germany.
Phone: +49-89-2178-2210 
Fax :  +49-89-2178-2211

Title: Towards a constructive definition of the compositional semantics

Abstract: Non monotonic negation plays an important role in logic programming for several reasons. First, it is a widespread form of negation in various forms of commonsense reasoning as well as in databases. Second, in spite of several attractive proposals, it has not been yet fully satisfactorily formalized, for some requirements that are natural from the viewpoint of applications are not fulfilled by the proposed semanitcs.

Reconsidering the issue with a strong bias towards applications, we proposed a "compositional semantics" in [1]. The compositional semantics aims at accomodating natural program composition requirement - called modularity requirement in [3] - and database integrity constraints. In a same formal framework, the compositional semantics accounts for disjunctive logic programs and database integrity constraints.

In this presentation, the compositional semantics as well as the considerations and results that led to its definition are recalled. It is first shown that the procedural semantics of (negation-free) logic programs can be formalized without calling for refutation proofs. That is, as opposed to what is usually assumed, classical logic negation is not needed for formalizing negation-free logic programs. Then it is shown that this gives rise to propose a notion of "local inconsistency" the appropriate one for formalizing negation and integrity constraints in logic programs and deductive databases. A model theory is introduced that accommodates local inconsistencies by means of so-called "weak" and "intended models". It is shown how this semantics generalises the completion [2] and stable semantics [4].

Then it is investigated how a fixpoint like, constructive definition of the intended models of the compositional semantics can be given. Thanks to the locality of inconsistencies, it is possible to generalize the usual bottom-up construction for stratified logic programs to logic programs and deductive databases with unrestricted forms of negation. It is investigated how the fixpoint like, constructive definition extends to disjunctive logic programs and to deductive databases including integrity constraints.


[1]  F. Bry
     A Compositional Semantics for Logic Programs
     and Deductive Databases.
     Proceedings of Joint International Conference and
     Symposium on Logic Programming, MIT Press, 1996.
[2]  K. Clark
     Negation as Failure.
     Logic and Databases
     293-322, Plenum Press, New York, 1978.
[3]  J. Dix
     A Classification-Theory of Semantics of Normal Logic
     Programs: I. Strong Properties, II. Weak Properties.
     Fundamentae Informatica.
     Vol. 22, No. 3, 227-288, 1995.
[4]  M. Gelfond and V. Lifschitz. 
     The Stable Model Semantics for Logic Programming.
     Proceedings of the  International Conference and Symposium
     on Logic Programming, MIT Press, 1988.

Weidong Chen <wchen@seas.smu.edu>

Department of Computer Science & Engineering
Southern Methodist University
Dallas, Texas 75275-0122, USA
Phone: (214) 768-3097
Fax: (214) 768-3085 

Title: Programming with Logical Queries, Bulk Updates and Hypothetical Reasoning

Abstract: This talk presents a language of update programs that integrates logical queries, bulk updates and hypothetical reasoning in a seamless manner. There is no syntactic or semantic distinction between queries and updates. Update programs extend logic programs with negation in both syntax and semantics. They allow bulk updates in which an arbitrary update is applied simultaneously for all answers of an arbitrary query. Hypothetical reasoning is naturally supported by testing the success or failure of an update. We describe an alternating fixpoint semantics of update programs and show that it can express all nondeterministic database transformations.

This report is available on-line as http://www.seas.smu.edu/~wchen/papers/updates.ps.gz

C. V. Damásio <cd@fct.unl.pt>

Departamento de Informática
Universidade Nova de Lisboa
P-2825 Monte da Caparica

Title: A non-monotonic logic program semantics and its implementation

Miscellaneous information: See the entry for Luís Moniz Pereira

Hendrik Decker < hendrik@zfe.siemens.de>

Siemens ZFE T SE 4

Title: Is Disjunction in Logic Programming Inclusive or Exclusive or What?

Abstract: In the field of disjunctive logic programming, it is very common to speak of "exclusive" and "inclusive" interpretations of disjunction. By several examples, we argue that it may be misleading or even counter-intuitive to speak of inclusivity or exclusivity with regard to the meaning of disjunction in the head of clauses. Likewise, it is misleading to associate the minimal model based GCWA with exclusive disjunction. For instance, the database

{ p v q, q v r, r v s }

has minimal models

{p, r}, {q, r}, {q, s}

The middle model interprets the middle clause of the database as an inclusive disjunction and the outer ones as exclusive. Since the middle model is preferred by many semantics, it exemplifies that it is doubtful to speak of an inclusive or exclusive semantics of disjunction at all. Another example: The database

{ p v q, q v r, r v p }

has minimal models

{p, q}, {q, r}, {r, p}

each of which is interpreting exactly one of the clauses inclusively and the others exclusively. The example shows that, in general, it does not make much sense to say that the GCWA "leads to an exclusive interpretation of Or", or even that "exclusive interpretation of Or leads to minimal models". The latter is not true, as can be seen when attempting to interpret each disjunction in the second database above as exclusive: There is no consistent all-exclusive interpretation. Also, to say that "the GCWA leads to a semantics which is as exclusive as possible" does not necessarily seem to be clear in general. For instance, the GCWA and the WGCWA as well as minimal and maximal models coincide and are the same for the two logically equivalent databases

{ p v p } and { p v false } [example by Ch. Sakama]

where the meaning of disjunction on the left is necessarily inclusive, and the meaning of disjunction on the right is necessarily exclusive.

The examples above suggest that it is more accurate to just speak of minimal models or maximal models (i.e., least Herbrand models of the `maximal version' of a program), for distinguishing different semantics of disjunctive logic programs. The terminology of "inclusive" and "exclusive" is appropriate only in some simple cases.

Thomas Eiter <eiter@vexpert.dbai.tuwien.ac.at>

Title: Expressiveness of partial disjunctive models on databases

Abstract: In this talk, we investigate the expressive power and complexity of partial model semantics for disjunctive deductive databases. In particular, partial stable, regular model, maximal stable (M-stable), and least undefined stable (L-stable) semantics for function-free disjunctive logic programs are considered, for which the expressiveness of queries based on possibility and certainty inference is determined. The analysis pays particular attention to the impact of syntactical restrictions on programs in the form of limited use of disjunction and negation. It appears that the considered semantics capture complexity classes at the lower end of the polynomial hierarchy. In fact, each class of the up to its third level is captured by some semantics using appropriate syntactical restrictions. Partial stable models have exactly the same expressive power and complexity as total stable models, while a higher degree of expressiveness is obtained by the semantics which minimize undefinedness. In particular, L-stable semantics has the highest expressive power. An interesting result in this course is that, in contrast with total stable models, negation is for partial stable models more expressive than disjunction. The results of this paper complement and extend previous results, and contribute to a more complete picture of the computational aspects of disjunctive logic programming and databases, which supports in choosing an appropriate setting that fits the needs in practice.

This report is available on-line as ftp://ftp.dbai.tuwien.ac.at/pub/papers/eiter/cdtr9583.ps.Z

Miscellaneous information: The results are from joint research with Nicola Leone (TU Vienna) and Domenico Sacca (Univ. Calabria). This work and more results have been presented at the LID '96 (Logic in Databases) workshop.

Ulrich Furbach < uli@informatik.uni-koblenz.de>

University of Koblenz
Institute for Computer Science
Rheinau 1
56075 Koblenz, Germany
Phone: ++49 261 9119 433
Fax:   ++49 261 9119 496

Title: Calculi for Disjunctive Logic Programming

Abstract: For disjunctive logic programs there are several proposals for defining interpreters, like the nearHorn-Prolog-Family, SLI-Resolution, SLO-Resolution, Model Tree construction or Restart Model Elimination. There have been also different approaches to assign least fixpoints to disjunctive logic programs. This paper proves that there exists an efficient bottom up proof procedure, namely hyper tableaux, which can be understood as a direct implementation of some of the well known fixpoint iteration techniques. We relate the hyper tableaux calculus to state semantics and to model trees. Furthermore we show by a simple syntactic transformation that hyper tableaux can be understood as an extension of SLO-resolution.

Heinrich Herre and Gerd Wagner < herre@informatik.uni-leipzig.de>

Universitaet Leipzig
Institut fuer Informatik
Augustusplatz 10-11
04109 Leipzig

Title: Stable Generated Models of Generalized Logic Programs

Abstract: We present a general definition of stable generated models for extended generalized logic programs (EGLP) which a) subsumes the notion of stable model for normal logic programs (in the sense of Gelfond-Lifschitz) and contains the answer set semantics for extended disjunctive logic programs; and b) allowing for arbitrary (open) formulas in the body and the head of a rule (i.e. does not depend on the presence of any specicfic connective, nor any specific syntax of rules). The intuition underlying our notion of stability are the properties of groundedness and supportedness which capture the concept of rule-governed generation of factual knowledge. EGLP proves as a powerful general-purpose AI-reasoning system with a clear preferential semantics in the framework of partial logic and thus provides a foundation for practical knowledge-based reasoning. The talk was presented by H. Herre.

Nicola Leone <nik@si.deis.unical.it>

Information Systems Department
Technical University of Vienna
A-1040 Vienna

Title: Disjunctive Stable Models: Unfounded Sets, Fixpoint Semantics and Computation

Abstract: Disjunctive Deductive Databases (DDDBs) --- function-free disjunctive logic programs where negation may occur in the rule bodies --- have been recently recognized as a very powerful tool for knowledge representation and commonsense reasoning.

We focus on stable model semantics, which, for the time being, is the most widely acknowledged semantics for DDDBs.

A new notion of unfounded set for disjunctive programs is first presented. Then, two declarative characterizations of stable models in terms of unfounded sets are given. The former shows that the set of stable models coincides with the family of unfounded-free models (i.e., a model is stable iff it contains no unfounded atom). The second proves that stable models can be equivalently defined by a property of their false literals, as a model is stable if and only if the set of its false literals coincides with its greatest unfounded set.

The well-founded WP operator is then generalized to disjunctive logic programs and a fixpoint semantics for disjunctive stable models is provided.

Exploiting the above theoretical results, an algorithm for the computation of stable models is provided. Both soundness and completeness of the proposed method are proved.

The computational complexity of the main computational problems related to the presented concepts is also analyzed.

Miscellaneous information: This is a joint research with Pasquale Rullo and Francesco Scarcello. Part of the results presented in this talk appear in the proceedings of the conference ILPS'95.

Jorge Lobo <jorge@eecs.uic.edu>

Department of EECS
University of Illinois at Chicago
851 S. Morgan st., Room 1120 SEO
Chicago, Illinois 60607-7053

Title: A Calculus for Disjunctive Logic Programs

Miscellaneous information: See the entry for Chitta Baral

Norman McCain < mccain@cs.utexas.edu>

Norman McCain
University of Texas at Austin
Department of Computer Sciences
Taylor Hall
Austin, TX 78712-1188
tel: +1-512-471-9746

Title: Causal Explanation and Disjunctive Default Logic

Abstract: In this talk I report on joint work with Hudson Turner. We define two logical systems --- one non-modal and one modal --- in which the central syntactic and semantic notions are those of a causal theory and a causally explained interpretation, respectively. Roughly, we say that a propositional interpretation I is causally explained by a causal theory T if every proposition that is true in I is caused to be true in I according to T. Given a language whose atoms are formed from fluents subscripted by times, we identify the world histories that are possible according to a causal theory T with the interpretations that are causally explained by T. Of our two logical systems, the modal one, which we call CEL (for Causal Explanation Logic), is more expressive. Under a modal encoding due to Hector Geffner (AAAI-90), it is shown to properly extend the non-modal one. We conclude by presenting a theorem, due to Hudson Turner, which demonstrates a close connection between CEL and disjunctive default logic.

Jack Minker < minker@cs.umd.edu>

Department of Computer Science and
Institute for Advanced Computer Studies 
University of Maryland
College Park, MD 20742  

Title: Logic and Databases: a 20 Year Retrospective

Abstract: At a workshop held Toulouse, France in 1977, Gallaire, Minker and Nicolas stated that logic and databases was a field in its own right. This was the first time that this designation was made. The impetus for this started approximately twenty years ago in 1976 when I visited Gallaire and Nicolas in Toulouse, France, which culminated in a workshop held in Toulouse, France in 1977. It is appropriate, then to provide an assessment as to what has been achieved in the twenty years since the field started as a distinct discipline. In this retrospective I shall review developments that have taken place in the field, assess the contributions that have been made, consider the status of implementations of deductive databases and discuss the future of work in this area.

This report is available on-line from http://www.cs.umd.edu/~minker/

Gerd Neugebauer < gerd@informatik.uni-koblenz.de>

Fachbereich Informatik
Universität Koblenz-Landau
Rheinau 1
56075 Koblenz
Tel: +49-261-9119 446
Fax: +49-261-9119 496

Title: Deductive Techniques for Information-Management-Systems

Abstract: Logic programming techniques can be used as a basis for an information management system. For this purpose it is necessary to provide means to incorporate heterogeneous sources of external information into a logic programming system.

This talk presents the approach used by the author for this purpose. It also features the angles and pitfalls with which we are faced when we work on a real application.

This report is available on-line as http://www.uni-koblenz.de/~gerd/Papers/glue.ps.gz

Miscellaneous information: The slides are availlable from the URL http://www.uni-koblenz.de/~gerd/ftp/GLUE/Slides/dagstuhl-96.ps.gz.

Ilkka Niemelä < ini@informatik.uni-koblenz.de>

University of Koblenz                 
Department of Computer Science        
Rheinau 1
D-56075 Koblenz, Germany   
tel: +49-261-9119-649
fax: +49-261-9119-496

Title: Towards Implementing Disjunctive Logic Programs using Hyper Tableaux

Abstract: Circumscriptive (minimal model) reasoning is identified as a key computational task in implementing leading semantics of disjunctive logic programs. Hyper tableaux, which combine hyper resolution and analytic tableaux, are put forward as a basis for a circumscriptive proof method. A new technique for extending tableau calculi to handle circumscriptive inference is proposed. The technique is based on a novel characterization of minimal models and it enables implementation of circumscriptive inference with low space complexity as the branches can be constructed "one at a time". Using this technique first-order parallel circumscription with fixed and varying predicates with respect to Herbrand models can be treated. The method is sound in the general case and complete when no function symbols are allowed.

Miscellaneous information: There are two reports related to the talk:

A Tableau Calculus for Minimal Model Reasoning
Appears in Proceedings of the Fifth Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Palermo, Italy, May 15-17, 1996, Springer-Verlag, 1996

Implementing Circumscription Using a Tableau Method
Appears in Proceedings of the European Conference on Artificial Intelligence. Budapest, Hungary, Aug 12-16, 1996, John Wiley, 1996

Luigi Palopoli < palopoli@si.deis.unical.it>

Title: Tractable disjunctive logic programming

Abstract: Implementing disjunctive logic programming is a highly complex task. Several tractable subsets of disjunctive logic programming have been proposed, but all of them implies significant limitations in expressive power. In this paper we devise an algorithm which always runs in polynomial time and realizes non-deterministic reasoning for an interesting class of disjunctive logic programs with function symbols. We show that the functional fragment of this class captures all polynomial time queries.

Miscellaneous information: The paper appears in the Proc. of the European Conf. on Artificial Intelligence, Budapest, August 1996.

Christian Papp <papp@uaic.ro>

Universitatia "Al. J. Cuza"
Jasi, Romania 

Title: Hypothesis of complete and partially complete information

Abstract: While default and autoepistemic logic have received a great interest from researchers, CWA and its generalizations were less considered in the literature. Only CWA and GCWA were iterated on stratified programs.

In this paper, we present two families of logics which can be obtained from the nonmonotonic logics used to reason with postitive programs (CWA, GCWA, WGCWA, and EGCWA) adn their 3-valued versions by performing two kinds of operations: iteration and stable extension. Iteration is suitable in the context of stratified programs. Stable extensions are defined recursively and do not make use if modal operators.

A parametrical definition of several known semantics for normal and disjunctive logic programs is this way obtained.

David Pearce <pearce@dfki.uni-sb.de>

German Research Centre for Artificial Intelligence (DFKI)
Stuhlsatzenhausweg 3
66123 Saarbrücken

Title: A new logical characterisation of stable models

Abstract: This paper relates inference in extended logic programming with nonclassical, nonmonotonic logics. We define a nonmonotonic logic, called equilibrium logic, based on the least constructive extension, N2, of the intermediate logic of "here-and-there". We show that on logic programs equilibrium logic coincides with the inference operation associated with the stable model and answer set semantics of Gelfond and Lifschitz. We thereby obtain a very simple characterisation of answer set semantics as a form of minimal model reasoning in N2, while equilibrium logic itself provides a natural generalisation of this semantics to arbitrary theories. We discuss briefly some consequences and applications of this result.

Luís Moniz Pereira <lmp@fct.unl.pt>

Departamento de Informática
Universidade Nova de Lisboa
P-2825 Monte da Caparica

Title: A non-monotonic logic program semantics and its implementation

Abstract: A semantics for non-monotonic logic programming including explicit negation, integrity constraints, and belief revision was presented. Correct top-down procedures for this semantics and the belief revision methods were presented too, as well as their implementation in prolog, plus examples of application.

Miscellaneous information: Joint work with J. J. Alferes and C. V. Damásio

Halina Przymusinska <halina@cs.ucr.edu>

California State Polytechnic University

Title: Towards a theory of elaboration tolerance: Logic Programming approach

Abstract: We present an attempt at mathematical investigation of software development process in the context of declarative logic programming. We introduce notions of specification and specification constructor which are developed from natural language description of the problem. Generalization of logic programs, called lp-functions are introduced to represent these specifications. We argue that the process of constructing lp-function by certain types of mathematical results which we call representation theorems and present some such theorems to illustrate the idea.

Miscellaneous information: Joint work with Michael Gelfond, University of Texas at El Paso

Teodor C. Przymusinski <teodor@cs.ucr.edu>

Title: Super-Logic Programs

Abstract: In order to demonstrate that a class of programs can be justifiably called an extension of logic programs one has to establish that:

In addition to these minimal and necessary requirements one should be able to argue that: In my talk I proposed a specific class of such extended logic programs which will be called super logic programs or just super-programs. I will argue that the class of super-programs satisfies all of the above conditions, and, in addition, is sufficiently flexible to allow various application-dependent extensions and modifications.

Miscellaneous information: Based on joint work with J.J. Alferes, S. Brass, J. Dix and L.M. Pereira

Dave Reed < reedd@dickinson.edu>

Dept. of Math and Computer Science
Dickinson College
Carlisle, PA  17013
Phone: (717) 245-1402
Fax:   (717) 245-1690 

Title: Incorporating Default Negation into Bidirectional Reasoning

Abstract: This talk addressed the use of negation as failure in the context of a SATCHMO-style theorem prover. SATCHMO (Manthey and Bry, 1988) is an elegant model-generation theorem prover, with one variant that combines the backward chaining of Prolog with forward chaining to implement bidirectional reasoning. Previous work (Loveland, Reed, and Wilson, 1995) has shown that relevancy testing can be incorporated into SATCHMO (SATCHMORE - SATCHMO with RElevancy), leading to much greater control over the forward chaining. Although SATCHMO (SATCHMORE) already incorporates classical negation, it is natural to consider the incorporation of default negation, especially the use of negation as failure as in Prolog. Unfortunately, the use of negation as failure in the backward chaining phase of SATCHMO can lead to inconsistent result. This is due to the fact that not all positive information is known in the backward chaining phase, since new facts may be asserted via forward chaining. However, if the clause set is locally stratified so that negative goals have their definitions contained entirely in the backward chaining component, then negation as failure is safe and behaves as expected.

Konstantinos Sagonas <kostis@CS.SunySB.Edu>

Department of Computer Science
University at Stony Brook
Stony Brook, NY 11790

Title: An Abstract Machine for Computing the Well-Founded Semantics

Abstract: In this talk we will present an implementation of the well-founded semantics in the SLG-WAM of XSB. To compute the well-founded semantics, the SLG-WAM adds to an efficient tabling engine three operations --- negative loop detection, delaying and simplification --- which serve to detect, to break and to resolve the cycles through negation that may arise in evaluating normal programs. We describe fully the addition of these operations to our tabling engine, and demonstrate the efficiency of our implementation in two ways. First, we present a theorem that bounds the need for delaying to those literals which are not dynamically stratified for a fixed-order computation. Secondly, we present performance results that indicate that the overhead of delaying and simplification to Prolog --- or tabled --- evaluations is minimal.

Miscellaneous information: This is joint work with Terrance Swift and David S. Warren.

An extended abstract of this paper appears under the same title in the proceedings of the 1996 Joint International Conference and Symposium on Logic Programming (published by The MIT Press).

John S. Schlipf <john.schlipf@uc.edu>

University of Cincinatti
Dept. of Computer Science
Cincinatti, OH 45221-0008

Title: Exploring closure properties in building stable models

Abstract: One way to grow stable models is to make tentative assignments of truth values as in the Davis-Putnam procedure. There it is always desirable to make all possible unit clause reductions before guess; here the analogue seems to be to close under on analouge of the well-founded semantics. For example, the system of Niemelä and Simons seems to do this. Unfortunately, due to non-monotonicity, the correctness of the procedure may not be obvious. We show this can be justified easily by studying the correct operator, in this case STp (I) + I, where STp (I) is the least model of the GL-transform of P w.r.t. I, and + is the lub in the knowledge ordering. (the same operator was also used by Seipel).

Dietmar Seipel < seipel@informatik.uni-wuerzburg.de>

Prof. Dr. Dietmar Seipel
Universität Würzburg
Institut für Informatik
Am Hubland
97074 Würzburg

Tel. +49 931 888 5026 Fax. +49 931 888 4600

Title: Model Generation for Disjunctive Deductive Databases

Abstract: This talk investigates two fixpoint approaches for minimal model reasoning with disjunctive deductive databases P. The first one, called model generation, is based on an operator Ti(P) defined on sets of Herbrand interpretations, whose least fixpoint is logically equivalent to the set of minimal Herbrand models of the database. The second approach, called state generation, uses a fixpoint operator Ts(P) based on hyperresolution. It operates on disjunctive Herbrand states and its least fixpoint is the set of logical consequences of P, the so-called minimal model state of the database.

We establish a useful correlation between hyperresolution by Ts(P) and model generation by Ti(P). Then we investigate the problem of continuity of the two operators Ts(P) and Ti(P). It is known that the operator Ts(P) is continuous, and so it reaches its least fixpoint in at most omega steps. On the other hand, the question of whether Ti(P) is continuous has been open. We show by a counterexample that Ti(P) is not continuous. Nevertheless, we prove that it converges towards its least fixpoint in at most omega steps too, as follows from the relationship that we show exists between hyperresolution and model generation.

This convergency result can be used to show that various kinds of computations that are related to model generation, e.g. the computation of perfect and stable models for normal-disjunctive deductive databases, reach their least fixpoints in at most omega steps.

Finally, based on an alternating fixpoint computation with Ti(P), we define a new well-founded semantics for normal-disjunctive deductive databases. This semantics, which we call alternating disjunctive well-founded semantics ADWFS, generalizes several well-known semantics - including the perfect model and the well-founded semantics - from the normal to the normal-disjunctive case. Furthermore, ADWFS is consistent for all normal-disjunctive databases without integrity constraints.

This report is available on-line from http://karna.cs.umd.edu:3264/projects/dddb.html

Miscellaneous information: The research on model generation and state generation was done in cooperation with Jack Minker and Carolina Ruiz from the University of Maryland at College Park, USA.

A research report on Model Generation and State Generation for Disjunctive Logic Programs is available at


Frieder Stolzenburg < stolzen@informatik.uni-koblenz.de>

Universität Koblenz-Landau
Rheinau 1
D-56075 Koblenz
Phone: +49+261-9119-426
Fax: +49+261-9119-496

Title: Computation of Non-Ground Disjunctive Well-Founded Semantic with Constraint Logic Programming (Jürgen Dix and Frieder Stolzenburg)

Abstract: Impressive work has been done in the last years concerning the meaning of negation and disjunction in logic programs, but most of this research concentrated on propositional programs only. While it suffices to consider the propositional case for investigating general properties and the overall behaviour of a semantics, we feel that for real applications and for computational purposes an implementation should be able to handle first-order programs.

In this talk we present a theoretical framework by defining a calculus of program transformations that apply directly to rules with variables and function symbols. Our main results are that (1) this calculus is confluent for arbitrary programs, (2) for finite ground programs it is equivalent to a terminating calculus introduced by Brass/Dix, and (3) it approximates a generalization of D-WFS for arbitrary programs.

We achieve this by transforming program rules into rules with equational constraints thereby using methods and techniques from constraint logic programming. In particular, disconnection-methods play a crucial role. This work might become the basis for a general combination of two paradigms: constraint logic programming and non-monotonic reasoning.

This report is available on-line as http://www.uni-koblenz.de/~stolzen/papers/nmelp96.ps.gz

Terrance Swift < tswift@cs.sunysb.edu>

 Computer Science Dept.
 SUNY Stony Brook
 Stony Brook, NY 11790-44400
 Phone: (001) 516-632-9801

Title: Taking I/O Seriously: Resolution Reconsidered for DISK I/O

Abstract: Modern compilation techniques can give Prolog programs, in the best cases, a speed comparable to C. However, Prolog has proven to be unacceptable for data-oriented queries for two major reasons: its sometimes poor termination and complexity properties for Datalog, and its tuple-at-a-time strategy. A number of tabling frameworks and systems have addressed the first problem, most notably the XSB system which has achieved Prolog speeds for tabled programs. However, tabling systems such as XSB continue to use the tuple-at-a-time paradigm. As a result, these systems may have poor complexity for aggregate optimization problems, and are not amenable to a tight interconnection with disk-resident data.

However, in a tabling framework, the difference between tuple-at-a-time behavior and set-at-a-time can be viewed as one of scheduling. Accordingly, we define a set-at-a-time tabling strategy and prove it iteration equivalent to a form of semi-naive magic evaluation. That is, we extend the well-known asymptotic results of Seki by proving that each iteration of the tabling strategy produces the same information as semi-naive magic. Further, this set-at-a-time scheduling is amenable to implementation in an engine that uses Prolog compilation. We describe both the engine, which is freely available, and its performance, which is comparable with the depth-first strategy even for in-memory Datalog queries. Because of its performance, and its fine level of integration of Prolog with a database-style search, the set-at-a-time engine appears as an important key to linking logic programming and deductive databases.

Mirek Truszczynski <mirek@cs.engr.uky.edu>

Computer Science Department
University of Kentucky
Lexington, KY 40506-0046

Title: Extremal problems in logic programming

Abstract: We discuss the following problem: given a class of (disjunctive) logic programs C, determine the maximum number of stable models (answer sets) of a program from C. We establish the maximum for the class of all logic programs with at most n clauses, and for the class of all logic programs of size at most n. We also characterize the programs for which the maxima are attained. We obtain similar results for the class of all disjunctive logic programs with at most n clauses, each of length at most m, and for the class of all disjunctive logic programs of size at most n. Our results on logic programs have direct implication for the design of algorithms to compute stable models. Several such algorithms, similar in spirit to the Davis-Putnam procedure, are described in the paper.

This report is available on-line as ftp://www.cs.engr.uky.edu/~ftp/cs/manuscripts/extremal.ps

Adnan H. Yahya < yahya@informatik.uni-muenchen.de >

Institut fur Informatik                  
Ludwig-Maximilians Universitat           
Oettingerstr. 67, 
D-80538, Munich, Germany       

Title: A Goal-Driven Approach to Efficient Query Processing in Disjunctive Databases.

Abstract: In query answering, approaches based on model generation tend to explore a much larger search space than is strictly needed. Top-down processing has a more focused search space which can, in many cases, result in more efficient query answering procedures. In this work a strong connection between model generation and clause derivability is established that allows the use of a (minimal) model generating procedure for evaluating queries in a top-down fashion. The advanced procedure requires no extensive rewriting of the input theory or the introduction of new predicates. Rather, it is based a certain duality principle for interpreting logical connectives of the theory. The dual theory is achieved by reversing the direction of the implication sign in all clauses representing the theory and the negation of the query. It is shown that a generic (minimal) model generating procedure operating on the transformed theory is equivalent to top-down query answering in the original theory. We explain the reasoning behind the advanced approach and show that it can be utilized for refined query answering by specifying the conditions under which the query becomes derivable from the theory.

This report is available on-line as http://www.pms.informatik.uni-muenchen.de/publikationen/PMS-FB/PMS-FB-1996-12.ps.gz

Jia-Huai You < you@cs.ualberta.ca>

GSB 615
Dept. Computing Science
University of Alberta
Edmonton, Alberta
Canada T6G 2H1

Title: Disjunctive Logic Programming by Constrained Monotonic Inferences

Abstract: We present a novel view of nonmonotonic reasoning based on monotonic inferences constrained by a simple notion of priority constraint. More important, we show that these type of constained inferences can be specified in a knowledge representation language where a theory consists of a collection of logic programming-like inference rules and a priority constraint among the rules. We demonstrate its applications to CWA, default reasoning, and circumscription. In particular we show that the answer set semantics of disjunctive logic programs can be represented by constrained monotonic inferences.

This report is available on-line from http://web.cs.ualberta.ca/~you/papers/pub.html

Miscellaneous information: The talk is based on joint work with Drs. Xianchang Wang and Li Yan Yuan.

Li-Yan Yuan <yuan@cs.ualberta.ca>

Department of Computing Science
University of Alberta
Edmonton, Canada  T6G 2H1 

Title: Accessibility Relation and Disjunctive Logic Programs

Abstract: By studying the accessibility relations in logic of belief, we reveal that almost all prominent declarative semantics of disjunctive logic programs can be characterized in terms of standard Kripke structures with different accessibility relations. Based on our understanding of belief, we impose a simple but very intuitive restriction on the accessibility relation for belief:

    An agent, being in world s, considers t as a possible belief
    world if and only if every belief held in t can be justified by
    facts and beliefs held in s.
Under this restriction, we are able to define three interesting classes of Kripke structures via various accessibility relations, and we further show that almost all prominent declarative semantics of disjunctive programs can be characterized by these three difference classes of Kripke structures. This result not just extends the expressive power of the Kripke structure but also clearly demonstrates that the nonmonotonic reasoning is a reasoning about implicit belief and therefore can be characterized by various logics of belief.

This report is available on-line as http://web.cs.ualberta.ca/~yuan/papers/dag96.ps

Back to the home page.
Maintained by: