This work develops an approach to qualitative belief revision in a fully probabilistic setting. We begin with a logic where possible worlds are assigned probabilities. In this logic an agent may believe a formula is true even though the subjective probability of the formula is less than 1.0. Similarly, after revision by a formula ϕ, the agent will believe ϕ is true, even though the agent’s subjective probability of ϕ may be less than 1.0. We establish a correspondence with the hallmark AGM postulates for belief revision. Moreover, we use Jeffrey Conditionalisation to establish a link with iterated belief change. To this end, we develop an approach that satisfies appropriately modified Darwiche-Pearl postulates (with clear justification). Thus, we provide a connection between quantitative probabilistic approaches on the one hand and the qualitative formulation of belief change, on the other. This work holds potential for the development of practical belief revision systems by applying a (qualitative) approach to belief change in probabilistic, uncertain domains.

We present an approach to incorporating qualitative assertions of conditional irrelevance into belief revision, in order to address the limitations of existing work which considers only unconditional irrelevance. These assertions serve to enforce the requirement of minimal change to existing beliefs, while also suggesting a route to reducing the computational cost of belief revision by excluding irrelevant beliefs from consideration. In our approach, a knowledge engineer specifies a collection of multivalued dependencies that encode domain-dependent assertions of conditional irrelevance in the knowledge base. We consider these as capturing properties of the underlying domain which should be taken into account during belief revision. We introduce two related notions of what it means for a multivalued dependency to be taken into account by a belief revision operator: partial and full compliance. We provide characterisations of partially and fully compliant belief revision operators in terms of semantic conditions on their associated faithful rankings. Using these characterisations, we show that the constraints for partially and fully compliant belief revision operators are compatible with the AGM postulates. Finally, we compare our approach to existing work on unconditional irrelevance in belief revision.

A major challenge in AI is dealing with uncertain information. While probabilistic approaches have been employed to address this issue, in many situations probabilities may not be available or may be unsuitable. As an alternative, qualitative approaches have been introduced to express that one event is no more probable than another. We provide an approach where an agent may reason deductively about notions of likelihood, and may hold beliefs where the subjective probability for a belief is less than 1. Thus, an agent can believe that p holds (with probability <1); and if the agent believes that q is more likely than p, then the agent will also believe q. Our language allows for arbitrary nesting of beliefs and qualitative likelihoods. We provide a sound and complete proof system for the logic with respect to an underlying probabilistic semantics, and show that the language is equivalent to a sublanguage with no nested modalities.

In general, an agent may have incomplete and inaccurate knowledge about its environment. As well, actions may not turn out as intended or may have nondeterministic effects, and sensors may on occasion give incorrect results. We present a general, qualitative approach to reasoning about action and change in such a setting. The approach is expressed as an extension to basic action theories in the situation calculus, where an agent's epistemic state is modelled by a set of situations, where each situation is assigned a non-negative integer representing its plausibility. The agent's epistemic state is updated by modifying these plausibility values after the execution of an action, taking into account the possibility of unexpected results. To this end, we consider actions to have an intensional aspect, under the control of and determined by the agent, and an extensional aspect, not directly accessible to the agent and controlled by "nature". This leads to two distinct but related related notions of belief, an extensional "bird's eye" view which models an agent's beliefs wrt actually-executed actions, and an intensional view representing beliefs from the agent's point of view. We argue that the approach is significantly more general and comprehensive than previous accounts, and leads to a unified view of failed actions and nondeterminism with respect to physical and sensing actions.

With the advent of artificial agents in everyday life, it is important that these agents are guided by social norms and moral guidelines. Notions of obligation, permission, and the like have traditionally been studied in the field of Deontic Logic, where deontic assertions generally refer to what an agent should or should not do; that is they refer to actions. In Artificial Intelligence, the Situation Calculus is (arguably) the best known and most studied formalism for reasoning about action and change. In this paper, we integrate these two areas by incorporating deontic notions into Situation Calculus theories. We do this by considering deontic assertions as constraints, expressed as a set of conditionals, which apply to complex actions expressed as GOLOG programs. These constraints induce a ranking of "ideality" over possible future situations. This ranking in turn is used to guide an agent in its planning deliberation, towards a course of action that adheres best to the deontic constraints. We present a formalization that includes a wide class of (dyadic) deontic assertions, lets us distinguish prima facie from all-things-considered obligations, and particularly addresses contrary-to-duty scenarios. We furthermore present results on compiling the deontic constraints directly into the Situation Calculus action theory, so as to obtain an agent that respects the given norms, but works solely based on the standard reasoning and planning techniques.

In this paper we present an approach to defeasible deontic inference. Given a set of rules R expressing conditional obligations and a formula A giving contingent information, the goal is to determine the most desirable outcome with respect to this information. Semantically, the rules R induce a partial preorder on the set of models, giving the relative desirability of each model. Then the set of minimal A models characterises the best that can be attained given that A holds. A syntactic approach is also given, in terms of maximal subsets of material counterparts of rules in R, and that yields a formula that expresses the best outcome possible given that A holds. These approaches are shown to coincide, providing an analogue to a soundness and completeness result. Complexity is not unreasonable, being at the second level of the polynomial hierarchy when the underlying logic is propositional logic. The approach yields desirable and intuitive results, including for the various “paradoxes” of deontic reasoning. The approach also highlights an interesting difference in how specificity is dealt with in nonmonotonic and deontic reasoning.

AGM contraction and revision assume an underlying logic that contains propositional logic. Consequently, this assumption excludes many useful logics such as the Horn fragment of propositional logic and most description logics. Our goal in this paper is to generalise AGM contraction and revision to (near-)arbitrary fragments of classical first-order logic. To this end, we first define a very general logic that captures these fragments. In so doing, we make the modest assumptions that a logic contains conjunction and that information is expressed by closed formulas or sentences. The resulting logic is called first-order conjunctive logic or FC logic for short. We then take as the point of departure the AGM approach of constructing contraction functions through epistemic entrenchment, that is the entrenchment-based contraction. We redefine entrenchment-based contraction in ways that apply to any FC logic, which we call FC contraction. We prove a representation theorem showing its compliance with all the AGM contraction postulates except for the controversial recovery postulate. We also give methods for constructing revision functions through epistemic entrenchment which we call FC revision; which also apply to any FC logic. We show that if the underlying FC logic contains tautologies then FC revision complies with all the AGM revision postulates. Finally, in the context of FC logic, we provide three methods for generating revision functions via a variant of the Levi Identity, which we call contraction, withdrawal and cut generated revision, and explore the notion of revision equivalence. We show that withdrawal and cut generated revision coincide with FC revision and so does contraction generated revision under a finiteness condition.

In artificial intelligence, a key question concerns how an agent may rationally revise its beliefs in light of new information. The standard (AGM) approach to belief revision assumes that the underlying logic contains classical propositional logic. This is a significant limitation, since many representation schemes in AI don’t subsume propositional logic. In this article, we consider the question of what the minimal requirements are on a logic, such that the AGM approach to revision may be formulated. We show that AGM-style revision can be obtained even when extremely little is assumed of the underlying language and its semantics; in fact, one requires little more than a language with sentences that are satisfied at models, or possible worlds. The classical AGM postulates are expressed in this framework and a representation result is established between the postulate set and certain preorders on possible worlds. To obtain the representation result, we add a new postulate to the AGM postulates, and we add a constraint to preorders on worlds. Crucially, both of these additions are redundant in the original AGM framework, and so we extend , rather than modify , the AGM approach. As well, iterated revision is addressed and the Darwiche/Pearl postulates are shown to be compatible with our approach. Various examples are given to illustrate the approach, including Horn clause revision, revision in extended logic programs, and belief revision in a very basic logic called literal revision .

In this paper we provide a general, unifying framework for probabilistic belief revision. We first introduce a probabilistic logic called p-logic that is capable of representing and reasoning with basic probabilistic information. With p-logic as the background logic, we define a revision function called p-revision that resembles partial meet revision in the AGM framework. We provide a representation theorem for p-revision which shows that it can be characterised by the set of basic AGM revision postulates. P-revision represents an "all purpose" method for revising probabilistic information that can be used for, but not limited to, the revision problems behind Bayesian conditionalisation, Jeffrey conditionalisation, and Lewis's imaging. Importantly, p-revision subsumes all three approaches indicating that Bayesian conditionalisation, Jeffrey conditionalisation, and Lewis' imaging all obey the basic principles of AGM revision. As well our investigation sheds light on the corresponding operation of AGM expansion in the probabilistic setting.

Forgetting is an operation on knowledge bases that has been addressed in different areas of Knowledge Representation and with respect to different formalisms, including classical propositional and first-order logic, modal logics, logic programming, and description logics. Definitions of forgetting have been expressed in terms of manipulation of formulas, sets of postulates, isomorphisms between models, bisimulations, second-order quantification, elementary equivalence, and others. In this paper, forgetting is regarded as an abstract belief change operator, independent of the underlying logic. The central thesis is that forgetting amounts to a reduction in the language, specifically the signature, of a logic. The main definition is simple: the result of forgetting a portion of a signature in a theory is given by the set of logical consequences of this theory over the reduced language. This definition offers several advantages. Foremost, it provides a uniform approach to forgetting, with a definition that is applicable to any logic with a well-defined consequence relation. Hence it generalises a disparate set of logic-specific definitions with a general, high-level definition. Results obtained in this approach are thus applicable to all subsumed formal systems, and many results are obtained much more straightforwardly. This view also leads to insights with respect to specific logics: for example, forgetting in first-order logic is somewhat different from the accepted approach. Moreover, the approach clarifies the relation between forgetting and related operations, including belief contraction.

The AGM paradigm of belief change studies the dynamics of belief states in light of new information. Finding, or even approximating, those beliefs that are dependent on or relevant to a change is valuable because, for example, it can narrow the set of beliefs considered during belief change operations. A strong intuition in this area is captured by Gärdenfors’s preservation criterion (GPC), which suggests that formulas independent of a belief change should remain intact. GPC thus allows one to build dependence relations that are linked with belief change. Such dependence relations can in turn be used as a theoretical benchmark against which to evaluate other approximate dependence or relevance relations. Fariñas and Herzig axiomatize a dependence relation with respect to a belief set, and, based on GPC, they characterize the correspondence between AGM contraction functions and dependence relations. In this paper, we introduce base dependence as a relation between formulas with respect to a belief base, and prove a more general characterization that shows the correspondence between kernel contraction and base dependence. At this level of generalization, different types of base dependence emerge, which we show to be a result of possible redundancy in the belief base. We further show that one of these relations that emerge, strong base dependence, is parallel to saturated kernel contraction. We then prove that our latter characterization is a reversible generalization of Fariñas and Herzig’s characterization. That is, in the special case when the underlying belief base is deductively closed (i.e., it is a belief set), strong base dependence reduces to dependence, and so do their respective characterizations. Finally, an intriguing feature of Fariñas and Herzig’s formalism is that it meets other criteria for dependence, namely, Keynes’s conjunction criterion for dependence (CCD) and Gärdenfors’s conjunction criterion for independence (CCI). We prove that our base dependence formalism also meets these criteria. Even more interestingly, we offer a more specific criterion that implies both CCD and CCI, and show our base dependence formalism also meets this new criterion.

We investigate minimization-based approaches to iterated belief change in multi-agent systems. A network of agents is represented by an undirected graph, where propositional formulas are associated with vertices. Information is shared between vertices via a procedure where each vertex minimizes disagreement with other vertices in the graph. Each iterative approach takes into account the proximity between vertices, with the underlying assumption that information from nearby sources is given higher priority than information from more distant sources. We have identified two main approaches to iteration: in the first approach, a vertex takes into account the information at its immediate neighbours only, and information from more distant vertices is propagated via iteration; in the second approach, a vertex first takes into account information from distance-1 neighbours, then from distance-2 neighbours, and so on, in a prioritized fashion. There prove to be three distinct ways to define the second approach, so in total we have four types of iteration. We define these types formally, find relationships between them, and investigate their basic logical properties. We also implemented the approaches in a software system called Equibel.

Belief revision has been studied mainly with respect to background logics that are monotonic in character. In this paper we study belief revision when the underlying logic is non-monotonic instead—an inherently interesting problem that is under explored. In particular, we will focus on the revision of a body of beliefs that is represented as a logic program under the answer set semantics, while the new information is also similarly represented as a logic program. Our approach is driven by the observation that unlike in a monotonic setting where, when necessary, consistency in a revised body of beliefs is maintained by jettisoning some old beliefs, in a non-monotonic setting consistency can be restored by adding new beliefs as well. We will define two revision functions through syntactic and model-theoretic methods respectively and subsequently provide representation theorems for characterising them.

In this paper we describe asprin, a general, flexible, and extensible framework for handling preferences among the stable models of a logic program. We show how complex preference relations can be specified through user-defined preference types and their arguments. We describe how preference specifications are handled internally by so-called preference programs, which are used for dominance testing. We also give algorithms for computing one, or all, optimal stable models of a logic program. Notably, our algorithms depend on the complexity of the dominance tests and make use of multi-shot answer set solving technology.

In this paper, we present an approach to forgetting in disjunctive logic programs, where forgetting an atom from a program amounts to a reduction in the signature of that program. Notably, the approach is syntax-independent, so that if two programs are strongly equivalent, then the result of forgetting a given atom in each program is also strongly equivalent. Our central definition of forgetting is abstract: forgetting an atom from program P is characterised by the set of those SE consequences of P that do not mention the atom to be forgotten. We provide an equivalent, syntactic, characterization in which forgetting an atom p is given by those rules in the program that do not mention p, together with rules obtained by a single inference step from those rules that do mention p. Forgetting is shown to have appropriate properties; in particular, answer sets are preserved in forgetting an atom. As well, forgetting an atom via the syntactic characterization results in a modest (at worst quadratic) blowup in the program size. Finally, we provide a prototype implementation of this approach to forgetting.

We consider the iterated belief change that occurs following an alternating sequence of actions and observations. At each instant, an agent has beliefs about the actions that have occurred as well as beliefs about the resulting state of the world. We represent such problems by a sequence of ranking functions, so an agent assigns a quantitative plausibility value to every action and every state at each point in time. The resulting formalism is able to represent fallible belief, erroneous perception, exogenous actions, and failed actions. We illustrate that our framework is a generalization of several existing approaches to belief change, and it appropriately captures the non-elementary interaction between belief update and belief revision.

In classical, AGM-style belief change, it is assumed that the underlying logic contains classical propositional logic. This is clearly a limiting assumption, particularly in Artificial Intelligence. Consequently there has been recent interest in studying belief change in approaches where the full expressivity of classical propositional logic is not obtained. In this paper we investigate belief contraction in Horn knowledge bases. We point out that the obvious extension to the Horn case, involving Horn remainder sets as a starting point, is problematic. Not only do Horn remainder sets have undesirable properties, but also some desirable Horn contraction functions are not captured by this approach. For Horn belief set contraction, we develop an account in terms of a model-theoretic characterisation involving weak remainder sets. Maxichoice and partial meet Horn contraction is specified, and we show that the problems arising with earlier work are resolved by these approaches. As well, constructions of the specific operators and sets of postulates are provided, and representation results are obtained. We also examine Horn package contraction, or contraction by a set of formulas. Again, we give a construction and postulate set, linking them via a representation result. Last, we investigate the closely-related notion of forgetting in Horn clauses. This work is arguably interesting since Horn clauses have found widespread use in AI; as well, the results given here may potentially be extended to other areas which make use of Horn-like reasoning, such as logic programming, rule-based systems, and description logics. Finally, since Horn reasoning is weaker than classical reasoning, this work sheds light on the foundations of belief change

We address the problem of belief change in (nonmonotonic) logic programming under answer set semantics. Our formal techniques are analogous to those of distance-based belief revision in propositional logic. In particular, we build upon the model theory of logic programs furnished by SE interpretations, where an SE interpretation is a model of a logic program in the same way that a classical interpretation is a model of a propositional formula. Hence we extend techniques from the area of belief revision based on distance between models to belief change in logic programs. We first consider belief revision: for logic programs P and Q , the goal is to determine a program R that corresponds to the revision of P by Q , denoted P * Q . We investigate several operators, including (logic program) expansion and two revision operators based on the distance between the SE models of logic programs. It proves to be the case that expansion is an interesting operator in its own right, unlike in classical belief revision where it is relatively uninteresting. Expansion and revision are shown to satisfy a suite of interesting properties; in particular, our revision operators satisfy all or nearly all of the AGM postulates for revision. We next consider approaches for merging a set of logic programs, P 1 , ..., P n . Again, our formal techniques are based on notions of relative distance between the SE models of the logic programs. Two approaches are examined. The first informally selects for each program P i those models of P i that vary the least from models of the other programs. The second approach informally selects those models of a program P 0 that are closest to the models of programs P 1 , ..., P n . In this case, P 0 can be thought of as a set of database integrity constraints. We examine these operators with regards to how they satisfy relevant postulate sets. Last, we present encodings for computing the revision as well as the merging of logic programs within the same logic programming framework. This gives rise to a direct implementation of our approach in terms of off-the-shelf answer set solvers. These encodings also reflect the fact that our change operators do not increase the complexity of the base formalism.

This paper presents an approach to belief revision in which revision is a function from a belief state and a finite set of formulas to a new belief state. In the interesting case, the set for revision S may be inconsistent but individual members of S are consistent. We argue that S will still contain interesting information regarding revision; in particular, maximum consistent subsets of S will determine candidate formulas for the revision process, and the agent’s associated faithful ranking will determine the plausibility of such candidate formulas. Postulates and semantic conditions characterizing this approach are given, and representation results are provided. As a consequence of this approach, we argue that revision by a sequence of formulas, usually considered as a problem of iterated revision, is more appropriately regarded as revision by the possibly-inconsistent set of these formulas. Hence we suggest that revision by a sequence of formulas is foremost a problem of (uniterated) set revision. 1

In action domains where agents may have erroneous beliefs, reasoning about the effects of actions involves reasoning about belief change. In this paper, we use a transition system approach to reason about the evolution of an agent's beliefs as actions are executed. Some actions cause an agent to perform belief revision while others cause an agent to perform belief update, but the interaction between revision and update can be non-elementary. We present a set of rationality properties describing the interaction between revision and update, and we introduce a new class of belief change operators for reasoning about alternating sequences of revisions and updates. Our belief change operators can be characterized in terms of a natural shifting operation on total pre-orderings over interpretations. We compare our approach with related work on iterated belief change due to action, and we conclude with some directions for future research.

Cryptographic protocols are usually specified in an informal, ad hoc language, with crucial elements, such as the protocol goal, left implicit. We suggest that this is one reason that such protocols are difficult to analyse, and are subject to subtle and nonintuitive attacks. We present an approach for formalising and analysing cryptographic protocols in a theory of action, specifically the situation calculus. Our thesis is that all aspects of a protocol must be explicitly specified. We provide a declarative specification of underlying assumptions and capabilities in the situation calculus. A protocol is translated into a sequence of actions to be executed by the principals, and a successful attack is an executable plan by an intruder that compromises the specified goal. Our prototype verification software takes a protocol specification, translates it into a high-level situation calculus (Golog) program, and outputs any attacks that can be found. We describe the structure and operation of our prototype software, and discuss performance issues.

Abstract An approach to the revision of logic programs under the answer set semantics is presented. For programs P and Q, the goal is to determine the answer sets that correspond to the revision of P by Q, denoted P * Q. A fundamental principle of classical (AGM) revision, and the one that guides the approach here, is the success postulate. In AGM revision, this stipulates that α ∈ K * α. By analogy with the success postulate, for programs P and Q, this means that the answer sets of Q will in some sense be contained in those of P * Q. The essential idea is that for P * Q, a three-valued answer set for Q, consisting of positive and negative literals, is first determined. The positive literals constitute a regular answer set, while the negated literals make up a minimal set of naf literals required to produce the answer set from Q. These literals are propagated to the program P, along with those rules of Q that are not decided by these literals. The approach differs from work in update logic programs in two main respects. First, we ensure that the revising logic program has higher priority, and so we satisfy the success postulate; second, for the preference implicit in a revision P * Q, the program Q as a whole takes precedence over P, unlike update logic programs, since answer sets of Q are propagated to P. We show that a core group of the AGM postulates are satisfied, as are the postulates that have been proposed for update logic programs.

In this paper we explore a class of belief update operators, in which the definition of the operator is compositional with respect to the sentence to be added. The goal is to provide an update operator that is intuitive, in that its definition is based on a recursive decomposition of the update sentence's structure, and that may be reasonably implemented. In addressing update, we first provide a definition phrased in terms of the models of a knowledge base. While this operator satisfies a core group of the benchmark Katsuno-Mendelzon update postulates, not all of the postulates are satisfied. Other Katsuno-Mendelzon postulates can be obtained by suitably restricting the syntactic form of the sentence for update, as we show. In restricting the syntactic form of the sentence for update, we also obtain a hierarchy of update operators with Winslett's standard semantics as the most basic interesting approach captured. We subsequently give an algorithm which captures this approach; in the general case the algorithm is exponential, but with some not-unreasonable assumptions we obtain an algorithm that is linear in the size of the knowledge base. Hence the resulting approach has much better complexity characteristics than other operators in some situations. We also explore other compositional belief change operators: erasure is developed as a dual operator to update; we show that a forget operator is definable in terms of update; and we give a definition of the compositional revision operator. We obtain that compositional revision, under the most natural definition, yields the Satoh revision operator.

The area of belief change studies how a rational agent may maintain its beliefs when obtaining or perceiving new information about the environment. This new information could include properties of the actual world, occurrences of events, and, in the case of multiple agents, actions performed by other agents, as well as the beliefs and preferences of other agents. Not surprisingly, this area has been of interest to researchers in different communities. The initial research in belief change came from the philosophical community, wherein belief change was studied generally from a normative point of view (i.e. providing axiomatic foundations about how rational agents should behave with respect to the information flux). Subsequently, computer scientists, especially in the artificial intelligence and the database communities, have been building on these results. Belief change, as studied by computer scientists, not only pays attention to behavioural properties characterizing evolving databases or knowledge bases, but must also address computational issues such as how to represent beliefs states in a concise way and how to efficiently compute the revision of a belief state. More recently, the economics and game theory community, in particular the emerging field of cognitive economics, has become active in belief change research, adopting a normative point of view, like philosophers, but paying more attention to the ‘cognitive plausibility’ or ‘fitness’ of the belief change operators.

We consider the problem of representing arbitrary preferences in causal reasoning and planning systems. In planning, a preference may be seen as a goal or constraint that is desirable, but not necessary, to satisfy. To begin, we define a very general query language for histories, or interleaved sequences of world states and actions. Based on this, we specify a second language in which preferences are defined. A single preference defines a binary relation on histories, indicating that one history is preferred to the other. From this, one can define global preference orderings on the set of histories, the maximal elements of which are the preferred histories. The approach is very general and flexible; thus it constitutes a ‘base’ language in terms of which higher-level preferences may be defined. To this end, we investigate two fundamental types of preferences that we call choice and temporal preferences. We consider concrete strategies for these types of preferences and encode them in terms of our framework. We suggest how to express aggregates in the approach, allowing, e.g. the expression of a preference for histories with lowest total action costs. Last, our approach can be used to express other approaches and so serves as a common framework in which such approaches can be expressed and compared. We illustrate this by indicating how an approach due to Son and Pontelli can be encoded in our approach, as well as the language PDDL3.

Reiter's default logic is one of the best known and most studied of the approaches to nonmonotonic reasoning. Several variants of default logic have subsequently been proposed to give systems with properties differing from the original. In this paper, we examine the relationship between default logic and its major variants. We accomplish this by translating a default theory under a variant interpretation into a second default theory, under the original Reiter semantics, wherein the variant interpretation is respected. That is, in each case we show that, given an extension of a translated theory, one may extract an extension of the original variant default logic theory. We show how constrained, rational, justified, and cumulative default logic can be expressed in Reiter's default logic. As well, we show how Reiter's default logic can be expressed in rational default logic. From this, we suggest that any such variant can be similarly treated. Consequently, we provide a unification of default logics, showing how the original formulation of default logic may express its variants. Moreover, the translations clearly express the relationships between alternative approaches to default logic. The translations themselves are shown to generally have good properties. Thus, in at least a theoretical sense, we show that these variants are in a sense superfluous, in that for any of these variants of default logic, we can exactly mimic the behaviour of a variant in standard default logic. As well, the translations lend insight into means of classifying the expressive power of default logic variants; specifically we suggest that the property of semi-monotonicity represents a division with respect to expressibility, whereas regularity and cumulativity do not.

We propose to formally represent time with structured temporal objects. Structured temporal objects denote related time intervals (and recursively, related temporal objects) which are conceived as structured objects, rather than relations among such intervals. The major emphasis in this approach is on temporal repetition. To that effect, a new temporal object, the time loop, is defined. The intent of a time loop is to capture a structured notion of repetition. We propose a first order theory formalizing these objects. The building blocks of this formalism are time intervals and Allen's qualitative interval relations. We prove a number of key desirable results including the consistency of the theory, and extensively compare expressions in this theory with previous related work. We argue that this theory presents temporality and temporal repetition in a simple, commonsense manner. Furthermore, we argue that it presents an alternative, succinct and more general view than previous proposals to represent temporal repetition.

We present a general approach for representing and reasoning with sets of defaults in default logic, focusing on reasoning about preferences among sets of defaults. First, we consider how to control the application of a set of defaults so that either all apply (if possible) or none do (if not). From this, an approach to dealing with preferences among sets of default rules is developed. We begin with an ordered default theory, consisting of a standard default theory, but with possible preferences on sets of rules. This theory is transformed into a second, standard default theory wherein the preferences are respected. The approach differs from other work, in that we obtain standard default theories and do not rely on prioritized versions of default logic. In practical terms this means we can immediately use existing default logic theorem provers for an implementation. Also, we directly generate just those extensions containing the most preferred applied rules; in contrast, most previous approaches generate all extensions, then select the most preferred. In a major application of the approach, we show how semimonotonic default theories can be encoded so that reasoning can be carried out at the object level. With this, we can reason about default extensions from within the framework of a standard default logic. Hence one can encode notions such as skeptical and credulous conclusions, and can reason about such conclusions within a single extension.

In recent years, there has been a large amount of disparate work concerning the representation and reasoning with qualitative preferential information by means of approaches to nonmonotonic reasoning. Given the variety of underlying systems, assumptions, motivations, and intuitions, it is difficult to compare or relate one approach with another. Here, we present an overview and classification for approaches to dealing with preference. A set of criteria for classifying approaches is given, followed by a set of desiderata that an approach might be expected to satisfy. A comprehensive set of approaches is subsequently given and classified with respect to these sets of underlying principles.

In this paper, we show how an approach to belief revision and belief contraction can be axiomatized by means of quantified Boolean formulas. Specifically, we consider the approach of belief change scenarios, a general framework that has been introduced for expressing different forms of belief change. The essential idea is that for a belief change scenario (K, R, C), the set of formulas K, representing the knowledge base, is modified so that the sets of formulas R and C are respectively true in, and consistent with the result. By restricting the form of a belief change scenario, one obtains specific belief change operators including belief revision, contraction, update, and merging. For both the general approach and for specific operators, we give a quantified Boolean formula such that satisfying truth assignments to the free variables correspond to belief change extensions in the original approach. Hence, we reduce the problem of determining the results of a belief change operation to that of satisfiability. This approach has several benefits. First, it furnishes an axiomatic specification of belief change with respect to belief change scenarios. This then leads to further insight into the belief change framework. Second, this axiomatization allows us to identify strict complexity bounds for the considered reasoning tasks. Third, we have implemented these different forms of belief change by means of existing solvers for quantified Boolean formulas. As well, it appears that this approach may be straightforwardly applied to other specific approaches to belief change.

We introduce a methodology and framework for expressing general preference information in logic programming under the answer set semantics. An ordered logic program is an extended logic program in which rules are named by unique terms, and in which preferences among rules are given by a set of atoms of form s [pr ] t where s and t are names. An ordered logic program is transformed into a second, regular, extended logic program wherein the preferences are respected, in that the answer sets obtained in the transformed program correspond with the preferred answer sets of the original program. Our approach allows the specification of dynamic orderings, in which preferences can appear arbitrarily within a program. Static orderings (in which preferences are external to a logic program) are a trivial restriction of the general dynamic case. First, we develop a specific approach to reasoning with preferences, wherein the preference ordering specifies the order in which rules are to be applied. We then demonstrate the wide range of applicability of our framework by showing how other approaches, among them that of Brewka and Eiter, can be captured within our framework. Since the result of each of these transformations is an extended logic program, we can make use of existing implementations, such as dlv and smodels. To this end, we have developed a publicly available compiler as a front-end for these programming systems.

We investigate a formal representation of time units, calendars, and time unit instances as restricted temporal entities for reasoning about repeated events. We generalize Allen's interval relations to a class level, and based on interval classes we define time units. We examine characteristics of time units, and provide a categorization of the hierarchical relations among them. Hence we define an abstract hierarchical unit structure (a calendar structure) that expresses specific relations and properties among the units that compose it. Specific objects in the time line are represented based on this formalism, including nonconvex intervals corresponding to repeated events. A goal of this research is to be able to represent and reason efficiently about repetition in time.

The epistemic notions of knowledge and belief have most commonly been modeled by means of possible worlds semantics. In such approaches an agent knows (or believes) all logical consequences of its beliefs. Consequently, several approaches have been proposed to model systems of explicit belief, more suited to modeling finite agents or computers. In this paper a general framework is developed for the specification of logics of explicit belief. A generalization of possible worlds, called situations, is adopted. However the notion of an accessibility relation is not employed; instead a sentence is believed if the explicit proposition expressed by the sentence appears among a set of propositions associated with an agent at a situation. Since explicit propositions may be taken as corresponding to “belief contexts” or “frames of mind,” the framework also provides a setting for investigating such approaches to belief. The approach provides a uniform and flexible basis from which various issues of explicit belief may be addressed and from which systems may be contrasted and compared. A family of logics is developed using this framework, which extends previous approaches and addresses issues raised by these earlier approaches. The more interesting of these logics are tractable, in that determining if a belief follows from a set of beliefs, given certain assumptions, can be accomplished in polynomial time.

An approach to theorem proving for the class of normal conditional logics is presented. These logics have been shown to be appropriate for representing a wide variety of commonsense assertions, including default and prototypical properties, counterfactuals, notions of obligation, and others. the logics are based on a possible worlds semantics but unlike the better-known modal logics of necessity and possibility, they contain a binary “variable conditional” operator, ⟹, rather than a unary modal operator. the truth of a statement A ⟹ B depends both on the accessibility relation between worlds and on the proposition expressed by the antecedent A. The approach develops an extension of the semantic tableaux approach to theorem proving. Basically, it consists in attempting to find an interpretation which will falsify a sentence or set of sentences. If successful, then a specific falsifying truth assignment is obtained; if not, then the sentence is valid. Since this method is based directly on the notion of truth, it is arguably more natural and intuitive than those based on proof-theoretic methods. the approach has been proven correct for the class of normal conditional logics. In addition, it has been implemented and tested on a number of different logics. Various heuristics have been incorporated, and the implementation, while exponential in the worst case, is shown to be reasonably efficient for a large set of test cases.

Abstract This paper addresses the problem in inductive generalization of determining when a general hypothesis is supported by a particular instance. If we accept that, first, some facts do indeed support a general hypothesis and, second, that an instance that supports a hypothesis also supports all logical consequences of the hypothesis, then unintuitive and problematic results are immediately forthcoming. These assumptions lead, for example, to the conclusion that a blue Honda is confirming evidence for the hypothesis that ravens are black. This problem is variously known as the paradoxes of confirmation or Hempel's paradox. In this paper I develop a formal characterization of the problem. The assumption that whatever supports all classical consequences of the hypothesis is rejected. Rather, I argue that a weaker notion of consequence should be adopted for determining what consequences of a hypothesis are supported by the same evidence. An extant formal system for learning from examples is used to address these problems of evidential support, and it is shown that in this framework the problems do not arise.

In the past, Kripke structures have been used to specify the semantic theory of various modal logics. More recently, modal structures have been developed as an alternative to Kripke structures for providing the semantics of such logics. While these approaches are equivalent in a certain sense, it has been argued that modal structures provide a more appropriate basis for representing the modal notions of knowledge and belief. Since these notions, rather than the traditional notions of necessity and possibility, are of particular interest to artificial intelligence, it is of interest to examine the applicability and versatility of these structures. This paper presents an investigation of modal structures by examining how they may be extended to account for generalizations of Kripke structures. To begin with, we present an alternative formulation of modal structures in terms of trees; this formulation emphasizes the relation between Kripke structures and modal structures, by showing how the latter may be obtained from the former by means of a three‐step transformation. Following this, we show how modal structures may be extended to represent generalizations of possible worlds, and to represent generalizations of accessibility between possible worlds. Lastly, we show how modal structures may be used in the case of a full first‐order system. In all cases, the extensions are shown to be equivalent to the corresponding extension of Kripke structures.

A formal approach to the automatic generation and maintenance of integrity constraints in relational databases is presented. It is assumed that some portion of the database extension is known and that constraints are to be formed on the basis of this portion. Since this portion may be updated or new relations added to the database the set of hypothesised constraints may require occasional revision. The goal is this paper is to characterise those constraints that may potentially be formed on the basis of a part of the extension. Formal systems are derived by means of which the set of constraints that can be formed is precisely specified. A procedure is derived for restoring the consistency of a set of constraints after conflicting tuples are encountered. It is shown that the set of constraints to which the procedure may be applied corresponds with minor limitations to the sentences of relational algebra.

A formal, foundational approach to autonomous knowledge acquisition is presented. In particular, “learning from examples” and “learning from being told” and the relation of these approaches to first‐order representation systems are investigated. It is assumed initially that the only information available for acquisition is a stream of facts, or ground atomic formulae, describing a domain. On the basis of this information, hypotheses expressed in set‐theoretic terms and concerning the application domain may be proposed. As further instances are received, the hypothesized relations may be modified or discarded, and new relations formed. The intent though is to characterize those hypotheses that may potentially be formed, rather than to specify the subset of the hypotheses that, for whatever reason, should be held. Formal systems are derived by means of which the set of potential hypotheses is precisely specified, and a procedure is derived for restoring the consistency of a set of hypotheses after conflicting evidence is encountered. In addition, this work is extended to where a learning system may be “told” arbitrary sentences concerning a domain. Included in this is an investigation of the relation between acquiring knowledge and reasoning deductively. However, the interaction of these approaches leads to immediate difficulties which likely require informal, pragmatic techniques for their resolution. The overall framework is intended both as a foundation for investigating autonomous approaches to learning and as a basis for the development of such autonomous systems.