In this paper, we present several extensions of epistemic logic with update operators modelling public information change. Next to the well-known public announcement operators, we also study public substitution operators. We prove many of the results regarding expressivity and completeness using so-called reduction axioms. We develop a general method for using reduction axioms and apply it to the logics at hand.

Although formal system verification has been around for many years, little attention was given to the case where the specification of the system has to be changed. This may occur due to a failure in capturing the clients’ requirements or due to some change in the domain (think for example of banking systems that have to adapt to different taxes being imposed). We are interested in having methods not only to verify properties, but also to suggest how the system model (...) should be changed so that a property would be satisfied. For this purpose, we will use techniques from the area of Belief Revision, that deals with the problem of changing a knowledge base in view of new information. In the last thirty years, several authors have contributed with change operations and ways of characterizing them. However, most of the work concentrates on knowledge bases represented using classical propositional logic. In the last decade, there have been efforts to apply belief revision theory to description and modal logics. In this work, we analyze what is needed for a theory of belief revision which can be applied to the temporal logic, such as the Computation Tree Logic (CTL). In particular, we illustrate different alternatives for formalizing the concept of revision of CTL. Our interest in this particular logic comes both from practical issues, since it is used for software specification, as from theoretical issues, as it is a non-compact logic and most existing results rely on compactness. We focus here on the revision of CTL models and present a characterization result for the revision of partial models. (shrink)

We prove that for any finite deduction structure there exists a unique concise-widest chain-preserved split. Based on this result, we propose a logical splitting strategy which enables an agent to split its belief structure such that all the original inference chains can be preserved. The significance of such logical splitting at least is four-fold: It can be used by an agent to separate its concerns appropriately, or even create smaller and smarter clones which could save time and efforts in their (...) deliberation computing; It will enable an agent to adjust its concerns dynamically based on its recognition of the current situation, which may further enable the agent to make rapid and rational decisions when situation shifting occurs; In periodic team synchronization domains where agents can periodically synchronize their behaviors with no restriction on communication, it can be employed as a critical process for maintaining the shared mental models among a team of agents; and It is helpful in alleviating the complexity of reasoning about relevant information, and in better anticipating both explicit and implicit information needs based on the recognition of the current situation. (shrink)

Suppositions can be introduced in either the indicative or subjunctive mood. The introduction of either type of supposition initiates judgments that may be either qualitative, binary judgments about whether a given proposition is acceptable or quantitative, numerical ones about how acceptable it is. As such, accounts of qualitative/quantitative judgment under indicative/subjunctive supposition have been developed in the literature. We explore these four different types of theories by systematically explicating the relationships canonical representatives of each. Our representative qualitative accounts of indicative (...) and subjunctive supposition are based on the belief change operations provided by AGM revision and KM update respectively; our representative quantitative ones are offered by conditionalization and imaging. This choice is motivated by the familiar approach of understanding supposition as `provisional belief revision' wherein one temporarily treats the supposition as true and forms judgments by making appropriate changes to their other opinions. To compare the numerical judgments recommended by the quantitative theories with the binary ones recommended by the qualitative accounts, we rely on a suitably adapted version of the Lockean thesis. Ultimately, we establish a number of new results that we interpret as vindicating the often-repeated claim that conditionalization is a probabilistic version of revision, while imaging is a probabilistic version of update. (shrink)

One of the standard principles of rationality guiding traditional accounts of belief change is the principle of minimal change: a reasoner's belief corpus should be modified in a minimal fashion when assimilating new information. This rationality principle has stood belief change in good stead. However, it does not deal properly with all belief change scenarios. We introduce a novel account of belief change motivated by one of Grice's maxims of conversational implicature: the reasoner's belief corpus is modified in a minimal (...) fashion to assimilate exactly the new information. In this form of belief change, when the reasoner revises by new information p ∨ q their belief corpus is modified so that p∨q is believed but stronger propositions like p∧q are not, no matter what beliefs are in the reasoner's initial corpus. We term this conservative belief change since the revised belief corpus is a conservative extension of the original belief corpus given the new information. (shrink)

We present a method for relevance sensitive non-monotonic inference from belief sequences which incorporates insights pertaining to prioritized inference and relevance sensitive, inconsistency tolerant belief revision. Our model uses a finite, logically open sequence of propositional formulas as a representation for beliefs and defines a notion of inference from maxiconsistent subsets of formulas guided by two orderings: a temporal sequencing and an ordering based on relevance relations between the putative conclusion and formulas in the sequence. The relevance relations are ternary (...) (using context as a parameter) as opposed to standard binary axiomatizations. The inference operation thus defined easily handles iterated revision by maintaining a revision history, blocks the derivation of inconsistent answers from a possibly inconsistent sequence and maintains the distinction between explicit and implicit beliefs. In doing so, it provides a finitely presented formalism and a plausible model of reasoning for automated agents. (shrink)

Belief revision from the point of view of doxastic logic. Logic Journal of the IGPL, 3(4), 535–553. Segerberg, K. (1995). Conditional action. In G. Crocco, L. Fariñas, & A. Herzig (Eds.), Conditionals: From philosophy to computer science, Studies ...

The purpose of this paper is to introduce a form of update based on the minimization of the geodesic distance on a graph. We provide a characterization of this class using set- theoretic operators and show that such operators bijectively correspond to geodesic metrics. As distance is generated by distinguishability, our framework is appropriate in contexts where distance is generated by threshold, and therefore, when measurement is erroneous.

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. (shrink)