PCL on Saturday

Detailed program
Saturday July 27th, 2002
See also the unified by-slot program

Sessions take place in auditorium 7 unless otherwise indicated.

Session 1: Axioms

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.

Session 2: Models and Sets

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.

Session 3: Dynamics, Interaction and Nonmonotonicity

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.

Session 4: Panel and Other Issues

16:00-16:45  Panel: Paraconsistency and Logic Programming -- An Odd Couple or a Natural Pairing?

16:45-17:15  Discussion: Publication of Proceedings

17:15-17:30  Closing

19:00-21:00  Dinner

Room: Restaurant A Hereford Beefstouw