Defaults as restrictions on classical Hilbert-style proofs

Since the earliest formalisation of default logic by Reiter many contributions to this appealing approach to nonmonotonic reasoning have been given. The different formalisations are here presented in a general framework that gathers the basic notions, concepts and constructions underlying default logic. Our view is to interpret defaults as special rules that impose a restriction on the juxtaposition of monotonic Hubert-style proofs of a given logicL. We propose to describe default logic as a logic where the juxtaposition of default proofs is subordinate to a restriction condition . Hence a default logic is a pair (L, ) where properties of the logic , like compactness, can be interpreted through the restriction condition . Different default systems are then given a common characterization through a specific condition on the logicL. We also prove cumulativity for any default logic (L, ) by slightly modifying the notion of default proof. We extend, in fact, the language ofL in a way close to that followed by Brewka in the formulation of his cumulative default system. Finally we show the existence of infinitely many intermediary default logics, depending on and called linear logics, which lie between Reiter's and ukaszewicz' versions of default logic.Work carried out in the framework of the agreement between Italian PT Administration and FUBLaforia, Université Paris VI Pierre et Marie Curie, 4 Place Jussieu,Tour 46, 75252 Paris, France     

Modal nonmonotonic logics demodalized

The study of the relation between default logic and modal nonmonotonic logics has been mostly concerned with the task of translating default logic to autoepistemic or some other modal nonmonotonic logic. Here, we discuss the reverse problem, that is, the possibility of translating modal nonmonotonic logics into default-type systems formulated in the language without modal operators. To this end, we first consider a reformulation of both formalisms in terms of what we call default consequence relations. These consequence relations turn out to be especially suitable for studying default and modal nonmonotonic reasoning. We show, in particular, that different kinds of such reasoning naturally correspond to different structural rules imposed on default consequence relations. Our main results also demonstrate that all modal nonmonotonic objects considered have exact nonmodal counterparts. As an immediate consequence of these results, we obtain a method of reducing common types of modal nonmonotonic reasoning to nonmodal default reasoning.     

Completeness and Counter-Example Generations of a Basic Protocol Logic: (Extended Abstract)

We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a “trace” any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.     

Default reasoning by deductive planning

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 rather 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.This author was a visiting professor at the University of Darmstadt while parts of this work were being carried out. This author also acknowledges support from the Commission of the European Communities under grant no. ERB4001GT922433.     

Default logic as a query language

Research in nonmonotonic reasoning has focused largely on the idea of representing knowledge about the world via rules that are generally true but can be defeated. Even if relational databases are nowadays the main tool for storing very large sets of data, the approach of using nonmonotonic AI formalisms as relational database query languages has been investigated to a much smaller extent. In this work, we propose a novel application of Reiter's default logic by introducing a default query language (DQL) for finite relational databases, which is based on default rules. The main result of this paper is that DQL is as expressive as SO_∃∀ the existential-universal fragment of second-order logic. This result is not only of theoretical importance: We exhibit queries-which are useful in practice-that can be expressed with DQL and cannot with other query languages based on nonmonotonic logics such as DATALOG with negation under the stable model semantics. In particular, we show that DQL is well-suited for diagnostic reasoning     

Modular correctness proofs of behavioural implementations

We introduce a concept of behavioural implementation for algebraic specifications which is based on an indistinguishability relation (called behavioural equality). The central objective of this work is the investigation of proof rules which allow us to establish the correctness of behavioural implementations in a modular (and stepwise) way and, moreover, are practicable enough to induce proof obligations that can be discharged with existing theorem provers. Under certain conditions our proof technique can also be applied for proving the correctness of implementations based on an abstraction equivalence between algebras in the sense of Sannella and Tarlecki. The whole approach is presented in the framework of total algebras and first-order logic with equality. Received: 14 August 1995 / 1 April 1998     

An introduction to personalization and mass customization

In this article, we address the question of how efficiently Semantic Web (SW) reasoners perform in processing (classifying and querying) taxonomies of enormous size and whether it is possible to improve on existing implementations. We use a bit-vector encoding technique to implement taxonomic concept classification and Boolean-query answering. We describe the technique we have used, which achieves high performance, and discuss implementation issues. We compare the performance of our implementation with those of the best existing SW reasoning systems over several very large taxonomies under the exact same conditions for so-called TBox reasoning. The results show that our system is among the best for concept classification and several orders-of-magnitude more efficient in terms of response time for query answering. We present these results in detail and comment them. We also discuss pragmatic issues such as cycle detection and decoding.     

A generalization of analytic deduction via labelled deductive systems. Part I: Basic substructural logics

In this series of papers we set out to generalize the notion of classical analytic deduction (i.e., deduction via elimination rules) by combining the methodology of labelled deductive systems (LDS) with the classical systemKE. LDS is a unifying framework for the study of logics and of their interactions. In the LDS approach the basic units of logical derivation are not just formulae butlabelled formulae, where the labels belong to a given labelling algebra. The derivation rules act on the labels as well as on the formulae, according to certain fixed rules of propagation. By virtue of the extra power of the labelling algebras, standard (classical or intuitionistic) proof systems can be extended to cover a much wider territory without modifying their structure. The systemKE is a new tree method for classical analytic deduction based on analytic cut.KE is a refutation system, like analytic tableaux and resolution, but it is essentially more efficient than tableaux and, unlike resolution, does not require any reduction to normal form.We start our investigation with the family of substructural logics. These are logical systems (such as Lambek's calculus, Anderson and Belnap's relevance logic, and Girard's linear logic) which arise from disallowing some or all of the usual structural properties of the notion of logical consequence. This extension of traditional logic yields a subtle analysis of the logical operators which is more in tune with the needs of applications. In this paper we generalize the classicalKE system via the LDS methodology to provide a uniform refutation system for the family of substructural logics.The main features of this generalized method are the following: (a) each logic in the family is associated with a labelling algebra; (b) the tree-expansion rules (for labelled formulae) are the same for all the logics in the family; (c) the difference between one logic and the other is captured by the conditions under which a branch is declared closed; (d) such conditions depend only on the labelling algebra associated with each logic; and (e) classical and intuitionistic negations are characterized uniformly, by means of the same tree-expansion rules, and their difference is reduced to a difference in the labelling algebra used in closing a branch. In this first part we lay the theoretical foundations of our method. In the second part we shall continue our investigation of substructural logics and discuss the algorithmic aspects of our approach.     

Weakest pre-condition reasoning for Java programs with JML annotations

This paper distinguishes several different approaches to organising a weakest pre-condition (WP) calculus in a theorem prover. The implementation of two of these approaches for Java within the LOOP project is described. This involves the WP-infrastructures in the higher order logic of the theorem prover PVS, together with associated rules and strategies for automatically proving JML specifications for Java implementations. The soundness of all WP-rules has been proven on the basis of the underlying Java semantics. These WP-calculi are integrated with the existing Hoare logic, and together form a verification toolkit in PVS: typically one uses Hoare logic rules to break a large verification task up into smaller parts that can be handled automatically by one of the WP-strategies.     

模糊描述逻辑知识库查询蕴涵的判定方法

大规模领域本体的快速发展对语义Web领域的数据访问提出了更高的要求,而基本的本体推理服务已不能满足数据密集型应用中处理复杂查询(主要是合取查询)的迫切需要.为此,大量的研究工作集中在本体和描述逻辑知识库合取查询算法的设计实现上,并开发出了很多知识库存储和查询的实用工具.近来模糊本体和模糊描述逻辑的研究,特别是它们在处理语义Web中模糊信息方面,得到了广泛关注.文中重点研究了模糊SH这一族极富表达能力的描述逻辑知识库的合取查询问题,提出了相应的基于推演表的算法,证明了算法对于f-SHOIQ的真子逻辑的可靠性、完备性和可终止性.证明了算法对于f-SHOIQ是可靠的,并分析了导致算法不可终止的原因.对于该问题的数据复杂度,证明了当查询中不存在传递角色时其严格的CONP上限.对于联合复杂度,汪明了算法关于知识库和查询大小的CO3NEXPTIME时间复杂度上限.     

Querying datalog with arrays: Design and implementation issues

This paper deals with the implementation of logic queries where array structures are manipulated. Both top-down and bottom-up implementations of the presented logic language, called Datalog ^A , are considered. Indeed, SLD-resolution is generalized to realize Datalog ^A top-down query answering. Further, a fixpoint based evaluation of Datalog ^A queries is introduced, which forms the basis for efficient bottom-up implementation of queries obtained by generalizing rewriting techniques such as magic set method to the case of Datalog ^A programs.Work partially supported by a European Union grant under the EC-US project DEUS EX MACHINA: nondeterminism for deductive databases and by a MURST grant (40% share) under the project Sistemi formali e strumenti per basi di dati evolute.     

Modular specifications with supernormal defaults

We add a simple module system to specifications with supernormal defaults. It allows to distinguish between defining and calling occurrences of predicates. This greatly improves the understandability of large default specifications and especially helps to solve the problem of unwanted contrapositions of rules. Our approach is similar to the distinction between head and body of logic programming rules, but it works on the higher level of default theories. So our results can help to integrate both approaches — at least on the semantical side for specification purposes. We also clarify the relation to prioritized defaults and argue that modular specifications are often preferable. Finally, we give a theoretical basis for query evaluation.This work was partially supported by the CEC under the ESPRIT Working Group 6071 IS-CORE (Information Systems — COrrectness and REusability).     

Operational concepts of nonmonotonic logics part 1: Default logic

We give an introduction to default logic, one of the most prominent nonmonotonic logics. Emphasis is given to providing an operational interpretation for the semantics of default logic that is usually defined by fixed-point concepts (extensions). We introduce a process model that allows to exactly calculate the extensions of a default theory in a quite easy way. We give a prototypical implementation of processes in Prolog able to handle the examples that can be found in literature. Finally, we develop some theoretical results about default logic and give new simple proofs using the process model as a theoretical tool.