 | |
Sessions
take place in auditorium 7 unless otherwise indicated.| 08:55- | 09:00
| Opening
and Welcome |
| 09:00- | 09:30
| Philippe Besnard, U Potsdam,
Germany
Torsten
Schaub, U Potsdam, Germany
Hans
Tompits, Vienna U of Techn., Austria
Stefan
Woltran, Vienna U of Techn., Austria
Paraconsistent
reasoning via quantified boolean formulas, I:
Axiomatising signed systems
Signed
systems were introduced as a general, syntax-independent
framework for paraconsistent reasoning, that is, non-trivialised reasoning
from inconsistent information. In this paper, we show how the family of
corresponding paraconsistent consequence relations can be axiomatised by
means of quantified Boolean formulas. This approach has several benefits.
First, it furnishes an axiomatic specification of paraconsistent reasoning
within the framework of signed systems. Second, this axiomatisation allows
us to identify upper bounds for the complexity of the different signed
consequence relations. We strengthen these upper bounds by providing strict
complexity results for the considered reasoning tasks. Finally, we obtain
an implementation of different forms of paraconsistent reasoning by appeal
to the existing system QUIP. |
| 09:30- | 10:00
| Guo-Qiang Zhang, Case Western Reserve U, USA
Axiomatic
aspects of default inference
Properties
of classical (logical) entailment relation have been
well studied and well-understood, either with or without the presence of
logical connectives. There is, however, less uniform agreement on laws for
the nonmonotonic consequence relation. This paper studies axioms for
nonmonotonic consequences from a semantics-based point of view, focusing on
a class of mathematical structures for reasoning about partial information
without a predefined syntax/logic. This structure is called a default
structure. We study axioms for the nonmonotonic consequence relation
derived from extensions as in Reiter's default logic, using skeptical
reasoning, but extensions are now used for the construction of possible
worlds in a default information structure. In previous work we showed that
skeptical reasoning arising from default-extensions obeys a well-behaved
set of axioms including the axiom of cautious cut. We show here that,
remarkably, the converse is also true: any consequence relation obeying
this set of axioms can be represented as one constructed from skeptical
reasoning. We provide representation theorems to relate axioms for
nonmonotonic consequence relation and properties about extensions, and
provide a one-to-one correspondence between nonmonotonic systems which
satisfies the law of cautious monotony and default structures with unique
extensions. Our results give a theoretical justification for a set of basic
rules governing the update of nonmonotonic knowledge bases, demonstrating
the derivation of them from the more concrete and primitive construction of
extensions. It is also striking to note that proofs of the representation
theorems show that only shallow extensions are necessary, in the sense that
the number of iterations needed to achieve an extension is at most three.
All of these developments are made possible by taking a more liberal view
of consistency: consistency is a user defined predicate, satisfying some
basic properties. |
| 10:00- | 10:30
| Jørgen Villadsen, Techn. U of Denmark
A
paraconsistent higher order logic
Classical
logic predicts that everything (thus nothing useful at
all) follows from inconsistency. A paraconsistent logic is a logic where an
inconsistency does not lead to such an explosion, and since in practice
consistency is difficult to achieve there are many potential applications
of paraconsistent logics in knowledge-based systems, logical semantics of
natural language, etc. Higher order logics have the advantages of being
expressive and with several automated theorem provers available. Also the
type system can be helpful. We present a concise description of a
paraconsistent higher order logic with countable infinite indeterminacy,
where each basic formula can get its own indeterminate truth value (or as
we prefer: truth code). The meaning of the logical operators is new and
rather different from traditional many-valued logics as well as from logics
based on bilattices. The adequacy of the logic is examined by a case study
in the domain of medicine. Thus we try to build a bridge between the HOL
and MVL communities. A sequent calculus is proposed based on recent work by
Muskens. |
| 11:00- | 11:30
| Ofer Arieli, Academic
College of Tel-Aviv, Israel
Marc
Denecker, U Brussels (Libre), Belgium
Bert
Van Nuffelen, K.U. Leuven, Belgium
Maurice
Bruynooghe, K.U. Leuven, Belgium
Repairing
inconsistent databases: A model-theoretic approach and
abductive reasoning
In
this paper we consider two points of views to the problem of
coherent integration of distributed data. First we give a pure
model-theoretic analysis of the possible ways to "repair" a database. We do
so by characterizing the possibilities to "recover" consistent data from an
inconsistent database in terms of those models of the database that exhibit
as minimal inconsistent information as reasonably possible. Then we
introduce an abductive application to restore the consistency of a given
database. This application is based on an abductive solver (A-system) that
implements an SLDNFA-resolution procedure, and computes a list of
data-facts that should be inserted to the database or retracted from it in
order to keep the database consistent. The two approaches for coherent data
integration are related by soundness and completeness results. |
| 11:30- | 12:00
| Michael Maher, Loyola U Chicago, USA
A
model-theoretic semantics for defeasible logic
Defeasible
logic is an efficient logic for defeasible reasoning.
It is defined through a proof theory and, until now, has had no model
theory. In this paper a model-theoretic semantics is given for defeasible
logic. The logic is sound and complete with respect to the semantics. We
also briefly outline how this approach extends to a wide range of
defeasible logics. |
| 12:00- | 12:30
| Jan Maluszynski, Linköping U, Sweden
Aida
Vitória, Linköping U, Sweden
Defining
rough sets by extended logic programs
We
show how definite extended logic programs can be used for
defining and reason with rough sets. Moreover, a rough-set-specific query
language is presented and an answering algorithm is outlined. Thus, we not
only show a possible application of a paraconsistent logic to the field of
rough sets as we also establish a link between rough set theory and logic
programming, making possible transfer of expertise between both
fields. |
| 13:45- | 14:30
| Diderik
Batens, Ghent U, Belgium
Invited
talk: On a partial decision method for dynamic proofs
This
paper concerns a goal directed proof procedure for the
propositional fragment of the adaptive logic ACLuN1. At the propositional
level, it forms an algorithm for final derivability. If extended to the
predicative level, it provides a criterion for final derivability. This is
essential in view of the absence of a positive test. The procedure may be
generalized to all flat adaptive logics. |
| 14:30- | 15:00
| Dina Goldin, U Connecticut, USA
Peter
Wegner, Brown U, USA
Paraconsistency
of interactive computation
The
goal of computational logic is to allow us to model
computation as well as to reason about it. We argue that a computational
logic must be able to model interactive computation. We show that
first-order logic cannot model interactive computation due to the
incompleteness of interaction. We show that interactive computation is
necessarily paraconsistent, able to model both a fact and its negation, due
to the role of the world (environment) in determining the course of the
computation. We conclude that paraconsistency is a necessary property for a
logic that can model interactive computation. |
| 15:00- | 15:30
| François Bry, U Munich, Germany
An
almost classical logic for logic programming and nonmonotonic
reasoning
The
model theory of a first-order logic called N4 is introduced.
N4 does not eliminate double negations, as classical logic does, but
instead reduces fourfold negations. N4 is very close to classical logic: N4
has two truth values; implications are, in N4 like in classical logic,
material; and negation distributes over compound formulas in N4 as it does
in classical logic. Results suggest that the semantics of normal logic
programs is conveniently formalized in N4: Classical logic Herbrand
interpretations generalize straightforwardly to N4; the classical minimal
Herbrand model of a positive logic program coincides with its unique
minimal N4 Herbrand model; the stable models of a normal logic program and
its so-called complete minimal N4 Herbrand models coincide. |
| 16:00- | 16:45
| Panel:
Paraconsistency and Logic Programming -- An Odd Couple or a Natural
Pairing? |
| 16:45- | 17:15
| Discussion:
Publication of Proceedings |
Room:
Restaurant A Hereford Beefstouw | |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
