Entailment Systems for Default Reasoning

CASSANO, VALENTÍN; LOPEZ POMBO, CARLOS GUSTAVO; MAIBAUM, THOMAS S. E.

Salamanca

Workshop; Worshop on Algebraic Development Techniques; 2012

Software certification is a widespread concern in Software Engineering for, in many cases, the compliance of software with certain requirements becomes indispensable because of the tasks it is supposed to perform. Formal methods have provided a satisfactory toolset for coping with this issue. However, they are mostly based on monotonic logical frameworks. This imposes some considerations on the manipulation of the corpus of evidence justifying how a piece of software fulfills its critical properties. For example, additional evidence obtained about a software artifact, e.g., data gathered from further testing, possibly invalidates previous claims made about it. Within a monotonic reasoning framework, this vitiates further analysis from logical interest4. The need to create formal frameworks capable of dealing with such scenarios then becomes indispensable. Nonmonotonic reasoning emerged from the field of Artificial Intelligence. Originally, it was motivated by a prevailing discontent in the area with the limits of first order classical logic as a framework for reasoning about action and causation5. Albeit, this initial motivation was rapidly outgrown and nonmonotonic reasoning became a subject of study in its own right. In brief, nonmonotonic reasoning reflects the fact that reasoning is not in general reducible to the consequences obtainable from a set of definite claims. Instead, it is also being carried out under some judiciously chosen hypothesis. These are understood as tentative claims and, in view of their nature, are abandoned in the light of new evidence. In this last respect, nonmonotonic reasoning appears as an adequate framework for coping with the class of problems just presented. There exist several alternative formalizations of a nonmonotonic consequence relation, but in this work we will concentrate on default reasoning. This formal- ism was proposed originally by Reiter in [2] as a way of reasoning with incomplete information6. Intuitively, in such situations some surmises are posited to carry out further reasoning. As a result, in default reasoning, the premises of its consequence relation consist of a set of facts, conceived of as representing unalterable judgments, and a set of default rules, understood as conditionally supporting some tentative claims. These claims are not only sustained on the basis of prerequisite evidence, but also in the absence of evidence negating their justifications. In view of this, they become the origin of non-monotonicity, for this sustainability may be undermined by the addition of further claims. Now, no two conflicting tentative claims can be considered in the same situation. Namely, if such a circumstance occurs, then one of them is to be discarded in that situation. Hence, to each set of facts and default rules it is possible to associate the class of alternative situations that may arise because of conflicting tentative claims. These alternative situations are known as extensions. The consequences of some given premises are obtained either skeptically, or credulously, based on what can be demonstrated in every, or some, extension respectively. The most illustrative example of a default reasoning argument is explained in reference to the legal principle of Presumption of Innocence. This principle states that in the absence of further information, it should be sustained that anyone accused of committing a crime is innocent. Arguably, if obtained in this way, the innocence of the accused must be regarded as a tentative claim. That is, if at a trial sufficient convicting evidence is presented, the claim denoting the innocence of this person can no longer be sustained. This general form of reasoning is not only typical of default reasoning but also of software certification. As previously mentioned, in the latter, additional evidence possibly invalidates already established claims. Since its introduction, several distinct formalizations of Reiter?s original idea have been proposed. These have led to what nowadays forms a class of default reasoning formalisms. We regard these formalizations as problematic for they have been described from an operational point of view. We believe that this underlying approach mitigates against the study of general properties of default reasoning systems. This is particularly reflected in the study of the formal properties of consequence relations for them. In [3] Meseguer introduced a categorical definition of entailment systems as a syntactic counterpart of institutions [4] providing an extremely general and powerful tool for the study of the general properties of monotonic entailment relations. Following this approach we propose a categorical formalization of the concept of an entailment system for default reasoning. We elaborate on the way in which our approach tackles the previously mentioned problems and illustrate how most of the standard formalizations of default reasoning are captured by this formalization. Furthermore, we explain how the approach advocated here elucidates some considerations with respect to general properties of consequence relations for default reasoning, thus underpinning the study of these properties. References Gabbay, D.M., Woods, J.: Handbook of the History of Logic: The Many Valued and Nonmonotonic Turn in Logic. Volume 8. North-Holland, Amsterdam (2007) Reiter, R.: A logic for default reasoning. Artificial Intelligence 13(1-2) (1980) 81?132 Meseguer, J.: General logics. In: Logic Colloquium 1987. (1989) 275?329 Goguen, J.A., Burstall, R.M.: Introducing institutions. In: Logics of Programs. Volume 164 of LNCS. (1984) 221?256