Departamento de Mathemática Universidade de Évora P-7000 Évora Portugal
Title: A non-monotonic logic program semantics and its implementation
Miscellaneous information:
See the entry for
Luís Moniz Pereira
Fachbereich Informatik Universität Koblenz-Landau Rheinau 1 Koblenz D-56075 Germany. 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
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
University of Koblenz Institute for Computer Science Rheinau 1 Koblenz D-56075 Germany. 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
Rh. Kiryat Sefer 18/12 Rishon Le-Zion 75220 Israel
Title: BICONSEQUENCE RELATIONS FOR GENERAL LOGIC PROGRAMS
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.
Universität Hannover Institut für Informatik Lange Laube 22 D-30175 Hannover Germany 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.
Institut für Informatik Universität Leipzig Augustusplatz 10-11 D-04109 Leipzig Germany
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.
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.
References:
[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.
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
Departamento de Informática Universidade Nova de Lisboa P-2825 Monte da Caparica Portugal
Title: A non-monotonic logic program semantics and its implementation
Miscellaneous information:
See the entry for
Luís Moniz Pereira
Siemens ZFE T SE 4 München Germany
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
has minimal models 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
has minimal models
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
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.
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.
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.
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.
Information Systems Department Technical University of Vienna A-1040 Vienna Austria
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.
Department of EECS University of Illinois at Chicago 851 S. Morgan st., Room 1120 SEO Chicago, Illinois 60607-7053 U.S.A.
Title: A Calculus for Disjunctive Logic Programs
Miscellaneous information: See the entry for
Chitta Baral
Norman McCain University of Texas at Austin Department of Computer Sciences Taylor Hall Austin, TX 78712-1188 USA mccain@cs.utexas.edu 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.
Department of Computer Science and Institute for Advanced Computer Studies University of Maryland College Park, MD 20742 U.S.A.
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/
Fachbereich Informatik Universität Koblenz-Landau Rheinau 1 56075 Koblenz Germany 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.
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
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.
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.
German Research Centre for Artificial Intelligence (DFKI) Stuhlsatzenhausweg 3 66123 Saarbrücken Germany.
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.
Departamento de Informática Universidade Nova de Lisboa P-2825 Monte da Caparica Portugal
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
California State Polytechnic University U.S.A.
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 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:
Miscellaneous information:
Based on joint work with J.J. Alferes, S. Brass,
J. Dix and L.M. Pereira
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.
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).
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 ST
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
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
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.
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
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
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.
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:
This report is available on-line as
http://web.cs.ualberta.ca/~yuan/papers/dag96.ps
Teodor C. Przymusinski
<teodor@cs.ucr.edu>
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.
Dave Reed
<
reedd@dickinson.edu>
Dept. of Math and Computer Science
Dickinson College
Carlisle, PA 17013
Phone: (717) 245-1402
Fax: (717) 245-1690
Konstantinos Sagonas
<kostis@CS.SunySB.Edu>
Department of Computer Science
University at Stony Brook
Stony Brook, NY 11790
U.S.A.
John S. Schlipf
<john.schlipf@uc.edu>
University of Cincinatti
Dept. of Computer Science
Cincinatti, OH 45221-0008
U.S.A.
Dietmar Seipel
<
seipel@informatik.uni-wuerzburg.de>
Prof. Dr. Dietmar Seipel
Universität Würzburg
Institut für Informatik
Am Hubland
97074 Würzburg
Germany
http://karna.cs.umd.edu:3264/projects/dddb.html
Frieder Stolzenburg
<
stolzen@informatik.uni-koblenz.de>
Universität Koblenz-Landau
Rheinau 1
D-56075 Koblenz
Germany
Phone: +49+261-9119-426
Fax: +49+261-9119-496
Terrance Swift
<
tswift@cs.sunysb.edu>
Computer Science Dept.
SUNY Stony Brook
Stony Brook, NY 11790-44400
U.S.A.
Phone: (001) 516-632-9801
Mirek Truszczynski
<mirek@cs.engr.uky.edu>
Computer Science Department
University of Kentucky
Lexington, KY 40506-0046
U.S.A.
Adnan H. Yahya
<
yahya@informatik.uni-muenchen.de >
Institut fur Informatik
Ludwig-Maximilians Universitat
Oettingerstr. 67,
D-80538, Munich, Germany
Jia-Huai You
<
you@cs.ualberta.ca>
GSB 615
Dept. Computing Science
University of Alberta
Edmonton, Alberta
Canada T6G 2H1
Li-Yan Yuan
<yuan@cs.ualberta.ca>
Department of Computing Science
University of Alberta
Edmonton, Canada T6G 2H1
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.
Back to the home page.
Maintained by: