Deepak Kapur
-----
Titles and abstracts of papers in J. of Automated Reasoning, Vol. 15, No. 1
Vladimir Lifschitz (editor)
Preface to the Special Issue on Common Sense and Nonmonotonic Reasoning
Michael Thielscher and Torsten Schaub
Default Reasoning by Deductive Planning
1-40
Key words: default logics, deductive planning, credulous and skeptical
reasoning, logic programming
This paper deals with the automation of reasoning from incomplete
information by means of default logics. We provide proof
procedures for default logics' major reasoning modes, namely,
credulous and skeptical reasoning. We start by reformulating the
task of credulous reasoning in default logics as deductive
planning problems. This interpretation supplies us with several
interesting and valuable insights into the proof theory of
default logics. Foremost, it allows us to take advantage of the
large number of available methods, algorithms, and
implementations for solving deductive planning problems. As an
example, we demonstrate how credulous reasoning in certain
variants of default logic is implementable by means of a planning
method based on equational logic programming. In addition, our
interpretation allows us to transfer theoretical results, such as
complexity results, from the field of planning to that of default
logics. In this way, we have isolated two yet unknown classes of
default theories for which deciding credulous entailment is
polynomial. Our approach to skeptical reasoning relies on an
arbitrary method for credulous reasoning. It does not strictly
require the inspection of all extensions, nor does it strictly
require the computation of entire extensions to decide whether a
formula is skeptically entailed. Notably, our approach abstracts
from an underlying credulous reasoner. In this way, it can be
used to extend existing formalisms for credulous reasoning to
skeptical reasoning.
Franz Bader and Bernharad Hollunder
Priorities on Defaults with Prerequisites, and Their Application
in Treating Specificity in Terminological Default Logic,
41-68
Key words: terminological default logic, default theories with priorities,
knowledge representation
In a recent paper we have proposed terminological default logic
as a formalism that combines means both for structured
representation of classes and objects and for detailed
inheritance of properties. The major drawback that
terminological default logic inherits from general default logic
is that it does not take precedence of more specific defaults
over more general ones into account. This behavior has already
been criticized in the general context of default logic, but it
is all the more problematic in the terminological case where the
emphasis lies on the hierarchical organization of concepts. The
present paper addresses the problem of modifying terminological
default logic such that more specific defaults are preferred. We
assume that the specificity ordering is induced by the
hierarchical computing priorities. It turns out that the
existing approaches for expressing priorities between defaults do
not seem to be appropriate for defaults with prerequisites.
Therefore we shall consider an alternative approach for dealing
with prioritization in the framework of Reiter's default logic.
The formalism is presented in the general setting of default
logic where priorities are given by an arbitrary partial ordering
on the defaults. We shall exhibit some interesting properties of
the new formalism, compare it with existing approaches, and
describe an algorithm for computing extensions. In the
terminological case, we thus obtain an automated default
reasoning procedure that takes specificity into account.
Sakthi Subramanian
Mechanical Verification of Strategies
69-93
Key words: automated theorem proving, Boyer-Moore theorem prover,
artificial intelligence, common sense reasoning, planning
This paper presents a method of representing planning domains in
the Boyer-Moore logic so that we can prove mechanically whether a
strategy solves a problem. Current approaches require explicit
frame axioms and state constraints to be included as part of a
domain specification and use a programming language for
expressing strategies. These make it difficult to specify
domains and verify plans efficiently. Our method avoids explicit
frame axioms, since domains are specificed by programming an
interpreter for sequences of actions in the Boyer-Moore logic.
Strategies are represented as `planners,' Lisp programs that take
an initial state and other arguments as input and return a
sequence of actions that, when executed in the given initial
state, will bring about a goal state. Mechanical verification of
a strategy is accomplished by proving that the corresponding
planner solves all instances of the given problem. We illustrate
our approach by verifying strategies in some variations of the
blocks world.
T. Irisa Schaub
A New Methodology for Query Answering in Default Logics
via Structure-Oriented Theorem Proving
95-165
Key words:default logics, query answering, credulous reasoning,
theorem proving, connection method
We present a new approach to query answering in default logics.
The basic idea is to treat default rules as classical
implications along with some qualifying conditions restricting
the use of such rules while query answering. We accomplish this
by taking advantage of the conception of structure-oriented
theorem proving provided by Bibel's connection method. We show
that the structure-sensitive nature of the connection method
allows for an elegant characterization of proofs in default
logic. After introducing our basic method for query answering in
default logics, we present a corresponding algorithm and describe
its implementation. Both the algorithm and its implementation
are obtained by slightly modifying an existing algorithm and an
existing implementation of the standard connection method. In
turn, we give a couple of refinements of the basic method that
lead to conceptually different algorithms. The approach turns
out to be extraordinarily qualified for implementations by means
of existing automated theorem proving techniques. We
substantiate this claim by presenting implementations of the
various algorithms along with some experimental analysis. Even
though our method has a general nature, we introduce it in the
first part of this paper with the example of constrained default
logic. This default logic is tantamount to a variant due to
Brewka, and it coincides with Reiter's default logic and a
variant due to Lukaszewicz on a large fragment of default logic.
Accordingly, our exposition applies to these instances of default
logic without modifications.