Walking the Tightrope between Expressiveness and Uncomputability: AGM Contraction beyond the Finitary Realm

Abstract

Although there has been significant interest in extending the AGM paradigm of belief change beyond finitary logics, the computational aspects of AGM have remained almost untouched. We investigate the computability of AGM contraction on non-finitary logics, and show an intriguing negative result: there are infinitely many uncomputable AGM contraction functions in such logics. Drastically, even if we restrict the theories used to represent epistemic states, in all non-trivial cases, the uncomputability remains. On the positive side, we use Büchi automata to construct computable AGM contraction functions on Linear Temporal Logic (LTL).

1. Introduction

The field of Belief Change [ 1, 2, 3 ] investigates how to keep a corpus of beliefs consistent as it evolves. The field is mainly founded on the AGM paradigm [ 1 ], named after its authors’ initials, which distinguishes, among others, two main kinds of changes: belief revision, which consists in incorporating an incoming piece of information with the proviso that the updated corpus of beliefs is consistent; and belief contraction whose purpose is to retract an obsolete piece of information. In either case, the incurred changes should be minimized so that most of the original beliefs are preserved. This is known as principle of minimal change. Contraction is central as it can be used to define other forms of belief change. For example, belief revision can be defined in terms of contraction: first, remove information in conflict with the incoming belief via contraction, only then incorporate the incoming belief. When classical negation is at disposal, this recipe for defining revision from contraction is formalised via the Levi identity [ 4, 5 ].

The AGM paradigm prescribes rationality postulates that capture the principle of minimal change, and constructive functions that satisfy such postulates, called rational functions, as for instance partial meet [ 1 ], (smooth) kernel contraction [ 6 ], epistemic entrenchment [ 2 ] and Grove’s system of spheres [ 7 ]. Originally, the AGM paradigm was developed assuming some conditions about the underlying logic [ 2, 8 ]. Although these conditions cover some classical logics such as classical Propositional Logic and First Order Logic, they restrict the reach of the AGM paradigm into more expressive logics including several Descriptions Logics [ 9 ], Modal Logics [ 10 ] and Temporal Logics such as LTL, CTL and CTL* [ 11 ]. It turns out that the AGM paradigm is independent of such conditions [ 8 ], although rational contraction functions do not exist in every logic [ 8, 12 ]. Logics in which rational contraction functions do exist are dubbed AGM compliant [ 8 ]. As a result, several works have been dedicated to dispense with the AGM assumptions in order to extend the paradigm to more expressive logics: Horn logics [ 13, 14, 15 ], 22nd International Workshop on Nonmonotonic Reasoning, November 2-4, 2024, Hanoi, Vietnam * Corresponding author. $ [e-mail] (D. Klumpp); [e-mail] (J. S. Ribeiro) € https://dominik-klumpp.net/ (D. Klumpp); https://jandsonribeiro.github.io/home/ (J. S. Ribeiro)

0000-0003-4885-0728 (D. Klumpp); 0000-0003-1614-6808 (J. S. Ribeiro) © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). para-consistent logics [ 16 ], Description Logics [ 17, 12, 8 ], and non-compact logics [ 18 ]. See [ 19 ] for a discussion of several other works in this line.

Although much efort has been put into extending the AGM paradigm to more expressive logics, few works have investigated the computational aspects of the AGM paradigm such as [ 20, 21, 22 ]. All these works, however, focused on investigating the complexity of decision problems for some ifxed belief change operators on classical propositional logics and Horn. In light of the interest and efort of expanding the AGM paradigm for more expressive non-classical logics, it is paramount to comprehend the computational aspects of belief change in such more expressive logics. In this context, there is a central question that even precedes complexity: Computability / Efectiveness: Given a belief change operator ∘ , does there exist a Turing Machine that computes ∘ , and stops on all inputs?

The answer to the question above depends on two main elements: the underlying logic, and the chosen operator. Clearly, it only makes sense to answer such questions for logics that are AGM compliant. However, independently of the operator, the question is trivial for finitary logics, that is, logics whose language contains only finitely many equivalence classes, as it is the case of classical propositional logics. For non-finitary logics, by contrast, we show a disruptive result: AGM rational contraction functions sufer from uncomputability.

This first result uses all the expressive power of the underlying logic. To control computability, one could limit the space of epistemic states to some specific set of theories (logically closed set of sentences). However, we show that no matter how much we constrain the space of epistemic states, uncomputability still remains, as long as the restriction is not so severe that the space collapses back to the ifnitary case. Although this shows that uncomputability is unavoidable in all such expressive spaces, it is of extreme importance to identify how, and under which conditions, one can construct specific (families of) contraction functions that are computable. We investigate this question for Linear Temporal Logic (LTL), and we show that when representing epistemic states via Büchi automata [ 23 ], we can construct families of contraction functions that are computable within such a space. LTL is a very expressive logic used in a plethora of applications in Computer Science and AI. For example, LTL has been used for specification and verification of software and hardware systems [ 11 ], in business process models such as DECLARE [ 24 ], in planning and reasoning about actions [ 25, 26 ], and extending Description Logics with temporal knowledge [ 27, 28 ]. Büchi automata are endued with closure properties which allow for both efective reasoning and computable contraction functions.

Roadmap: In Section 2, we review basic concepts regarding logics, including LTL and Büchi automata. We briefly review AGM contraction in Section 3. Section 4 discusses the question of finite representation for epistemic states, and presents our first contribution, namely, we introduce a general notion to capture all forms of finite representations, and show a negative result: for a wide class of so-called compendious logics, not all epistemic states can be represented ifnitely. In Section 5, we present an expressive method of ifnite representation for LTL which is based on Büchi automata, and discuss how it supports reasoning. Section 6 introduces the notion of AGM closedness, i.e., every rational contraction outcome on a finitely representable belief state should again be finitely representable. We show that, under certain weak conditions, closedness cannot be satisfied for compendious logics. In Section 7, we establish our third negative result for compendious logics: even if we restrict ourselves to contraction functions whose output can be represented, uncomputability of contraction is inevitable in the non-finitary case, i.e., there always exist uncountably many uncomputable contraction functions. On the positive side, in Section 8, we show that computable contractions do exist for LTL theories represented via Büchi automata, and we identify the conditions needed for computability. Section 9 discusses the impact of our results and provides an outlook on future work.

A version of the paper including proofs is available [ 29 ].

2. Logics and Automata

We review a general notion of logics that will be used throughout the paper. We use () to denote the power set of a set . A logic is a pair L = (Fm, Cn) comprising a countable1 set of formulae Fm, and a consequence operator Cn : (Fm) → (Fm) that maps each set of formulae to the conclusions entailed from it. We sometimes write FmL and CnL for brevity.

We consider logics that are Tarskian, that is, logics whose consequence operator Cn is monotone (if 1 ⊆ 2 then Cn(1) ⊆ Cn(2)), extensive ( ⊆ Cn()) and idempotent (Cn(Cn()) = Cn()). We say that two formulae , ∈ Fm are logically equivalent, denoted ≡ , if Cn( ) = Cn( ). Cn(∅) is the set of all tautologies. A theory of L is a set of formulae such that Cn() = . The expansion of a theory by a formula is the theory + := Cn( ∪ { }). Let ThL denote the set of all theories of L. If ThL is finite, we say that L is finitary ; otherwise, L is non-finitary . Equivalently, L is finitary if L has only ifnitely many formulae up to logical equivalence.

A theory is consistent if ̸= Fm, and it is complete if for all formulae /∈ , we have + = Fm. The set of all complete consistent theories of L is denoted as CCTL. The set of all CCTs that do not contain is given by ( ).

A logic L is Boolean, if FmL is closed under the classical boolean operators and they are interpreted as usual. In particular, for a logic to be Boolean, we require every theory ∈ ThL to coincide with the intersection of all the CCTs containing , that is, = ⋂︀{ ′ ∈ CCTL | ⊆ ′ }. 1A set is countable if there is an injection from to the natural numbers.

We omit subscripts whenever the meaning is clear.

2.1. Linear Temporal Logic

We recall the definition of linear temporal logic [ 11 ], LTL for short. For the remainder of the paper, we fix an arbitrary ifnite, nonempty set AP of atomic propositions. Definition 1 (LTL Formulae). Let range over AP . The formulae of LTL are generated by the following grammar: ::= ⊥ | | ¬ | ∨ | X | U

FmLTL denotes the set of all LTL formulae.

In LTL, time is interpreted as a linear timeline that unfolds infinitely into the future. The operator X states that a formula holds in the next time step, while U means that holds until holds (and does eventually hold). We define the usual abbreviations for boolean operations ( ⊤, ∧, →) as well as the temporal operators F := ⊤ U (finally , at some point in the future), G := ¬F ¬ (globally, at all points in the future), and X for repeated application of X , where ∈ N.

Formally, timelines are modelled as traces. A trace is an infinite sequence = 01 . . ., where each ∈ (AP ) is a set of atomic propositions that hold at time step . The infinite sufix of starting at time step is denoted by = + · · · . The set of all traces is denoted by (AP ).

The semantics of LTL is defined in terms of Kripke structures [ 11 ], which describe possible traces.

Definition 2 (Kripke Structure). A Kripke structure is a tuple = (, , , ) such that is a finite set of states; ⊆ is a non-empty set of initial states; ⊆ × is a left-total transition relation, i.e., for all ∈ there exists ′ ∈ such that (, ′) ∈ ; and : → (AP ) labels states with sets of atomic propositions.

A trace of a Kripke structure is a sequence = (0) (1) (2) . . . with 0 ∈ , and for all ≥ 0, ∈ and (, +1) ∈ . The set of all traces from a Kripke structure is given by Traces ( ). Figure 1 shows an example of a Kripke structure, in graphical notation.

The satisfaction relation between Kripke structure and LTL formulae is defined in terms of the satisfaction between the Kripke structure’s traces and LTL formulae. Definition 3 (Satisfaction). The satisfaction relation between traces and LTL formulae is the least relation |= ⊆ (AP ) × FmLTL such that, for all traces = 01 . . . ∈ (AP ): ̸|= ⊥ |= |= ¬ |= 1 ∨ 2 |= X |= 1 U 2 if if if if if ∈ 0 ̸|= |= 1 or |= 2 1 |= there exists ≥ 0 s.t. |= 2 and for all < , |= 1

Some Infinite Words from ℒ(): ∅,{} 0 ∅,{} 1 {} |= , if all traces of satisfy . satisfies a set of formulae, |= , if |= for all ∈ . The consequence operator CnLTL is defined from the satisfaction relation.

Definition 4 (Consequence Operator). The consequence operator CnLTL maps each set of LTL formulae to the set of all formulae , such that for all Kripke structures , if |= then also |= .

Observation 5. LTL is Tarskian and Boolean.

2.2. Büchi Automata

Büchi automata are finite automata widely used in formal specification and verification of systems, specially in LTL model checking [ 11 ]. Büchi automata have also been used in planning to synthesize plans when goals are in LTL [ 26, 30 ]. Definition 6 (Büchi Automata). A Büchi automaton is a tuple = (, Σ , ∆ , 0, ) consisting of a finite set of states ; a finite, nonempty alphabet Σ (whose elements are called letters); a transition relation ∆ ⊆ × Σ × ; a set of initial states 0 ⊆ ; and a set of recurrence states ⊆ .

We show a concrete Büchi automaton in Example 7.

A Büchi automaton accepts an infinite word over a finite alphabet Σ , if the automaton visits a recurrence state infinitely often while reading the word. Formally, an inFor a finite word = 0 . . . , with ≥ ifnite word is a sequence 01 . . . with ∈ Σ the infinite word corresponding to the infinite repetition of . The set of all infinite words is denoted by Σ . An infinite word 012 . . . ∈ Σ is accepted by a Büchi automaton = (, Σ , ∆ , 0, ) if there exists a sequence 0, 1, 2, . . . of states ∈ such that 0 ∈ 0 is an initial state, for all we have that (, , +1) ∈ ∆ are infinitely many ∈ N with ∈ . The set ℒ() of all and there accepted words is the language of .

In this work, unless otherwise noted, we always consider 0, let denote for all .

Büchi automata over the alphabet Σ = letters are sets of atomic propositions and infinite words are traces. The following example presents such an automaton. (AP ), where instance, the sequence

Example 7. Figure 2 illustrates (on the left) a Büchi automa

ton over the alphabet Σ = {∅, {}}. States are depicted as circles and each transition (, , ′) is depicted as an arrow from to ′ labelled with . The initial state is 0, and the recurrence states are marked as double circles, i. e., 1 and 2.

The right-hand side of Figure 2 shows some of the infinite words accepted by the Büchi automaton . Consider, for 0 →∅ 0 →∅ 0 →∅ 1 {→} 2 →∅ 1 {→} 2 . . . , where each arrow → ′ indicates the transition (, , ′) in the automaton. By concatenating the letters in this sequence, we get the infinite word 1 defined in Figure 2. The acceptance condition requires some recurrence states to appear infinitely often. As for instance the recurrence state 1 appears infinitely often, the acceptance condition holds and 1 is accepted. Analogously, the infinite words 2 and 3 are also accepted.

On the other hand, the infinite word ′ = ∅ cepted, as the only sequence of states that produces this word is 0 →∅ 0 →∅ 0 . . ., where 0 →∅ loops. The only state in this sequence is 0 which is not a recurrence state and, therefore, is not acthe acceptance condition is violated.

Emptiness of a Büchi automaton’s language is decidable. Further, Büchi automata for the union, intersection and complement of the languages of given Büchi automata can be efectively constructed [ 23 ]. In the remainder of the paper we specifically make use of the construction for union ⊓ and intersection, and denote them with the symbol ⊔ resp.

. The automata-theoretic treatment for several crucial reasoning problems in LTL, such as model-checking and satisfiability, is based on the following result:

Proposition 8 ([11]). For every LTL formula and every

Kripke structure , there exist Büchi automata and

that accept precisely the traces that satisfy resp. the traces ∈ (AP ) | |= }, and of , that is, ℒ( ) = {

ℒ( ) = Traces ( ).

The proposition above states that every LTL formula can be expressed as a Büchi automaton , in the sense that accepts exactly all the traces satisfying . This result allows to decide if a formula is satisfiable, by deciding emptiness of ℒ( ). Analogously, a Büchi automaton can be used to capture precisely all the traces from a given Kripke structure , as Proposition 8 states. These two observations make it possible to decide LTL model-checking, by deciding the inclusion ℒ( ) ⊆ ℒ we will exploit Proposition 8 to devise mechanisms that support the computation of belief change operators in LTL. ( ). In Section 5, 3. AGM

Contraction

.

In the AGM paradigm, the epistemic state of an agent is represented as a theory. A contraction function for a theory is a function − : Fm

→ (Fm) that given an unwanted piece of information outputs a subset of which does not entail . Contraction functions are subject to the following rationality postulates [ 2 ]:

. (K−2 ) − ⊆ (K−1 ) − . = Cn( − ) (K−5 ) ⊆

( − ) + (K−3 ) If ̸∈ , then − = . (K−4 ) If ̸∈ Cn.(∅), then ̸∈ − (K−6 ) If .≡ , then . − = .− (K−7 ) ( − ) ∩ ( − ) ⊆ − . .

. . .

(closure) (inclusion) (vacuity) (success) (recovery) (extensionality) . ( ∧ ) . (K−8 ) If ̸∈ − ( ∧ ) then − ( ∧ ) ⊆ −

For a detailed discussion on the rationale of these postulates, see [ 1, 2, 3 ]. The postulates (K−1 ) to (K−6 ) are called the basic rationality postulates, while (K−7 ) and (K−8 ) are known as supplementary postulates. A contraction function that satisfies the basic rationality postulates is called a rational contraction function. If a contraction function satisfies all the eight rationality postulates, we say that it is fully rational.

There are many diferent constructions for (fully) rational AGM contraction such as Partial Meet [ 1 ], Epistemic Entrenchment [ 2 ], and Kernel Contraction [ 6 ]. All these functions are characterized by the AGM postulates of contraction. For an overview, see [ 31, 3 ]. These contraction functions, however, are rational only in very specific logics, precisely in the presence of the AGM assumptions [ 8 ] which includes requiring the logic to be Boolean and compact. See [ 8 ] for details about the AGM assumptions.

To embrace more expressive logics, Ribeiro et al. [ 18 ] have proposed a new class of (fully) rational contraction functions which only assume the underlying logic to be Tarskian and Boolean: the Exhaustive Contraction Functions (for basic rationality) and the Blade Contraction Functions (for full rationality). We briefly review Exhaustive Contraction Functions. We do not delve into the Blade Contraction Functions, as our results for full rationality do not use such functions, but rather use the supplementary postulates directly. Definition 9 (Choice Functions). A choice function is a function : Fm → (CCT) maps each formula to a set of complete consistent theories satisfying the following: (CF1) ( ) ̸= ∅; (CF2) if ̸∈ Cn(∅), then ( ) ⊆ ( ); and (CF3) for all ,

∈ Fm, if ≡ then ( ) = ( ).

A choice function chooses at least one complete consistent theory, for each formula to be contracted (CF1). As long as is not a tautology, the CCTs chosen must not contain the formula (CF2), since the goal is to relinquish . The last condition (CF3) imposes that a choice function is syntax-insensitive.

Definition 10 (Exhaustive Contraction Functions). Let be a choice function. The Exhaustive Contraction Fu.nction (ECF) on a theory induced by is the function − such . that − .= ∩ ⋂︀ ( ), if /∈ Cn(∅) and ∈ ; otherwise, − = .

Whenever the formula to be contracted is not a tautology and is in the theory , an ECF modifies the current theory by selecting some CCTs and intersecting them with . On the other hand, if is either a tautology or is not in the theory , then all beliefs are preserved. The ECFs are similar in spirit to the standard partial meet functions [ 1 ]. The main diference is that partial meet relies on the internal structure of the current theory by selecting and intersecting remainders (maximal non-entailing subsets), whilst ECF chooses external structures (CCTs). In the latter, CCTs are used, because, in the absence of compactness, remainders do not exist in general [ 12, 18, 32 ]. .

Theorem 11. [ 18 ] A contraction function − is rational if it is an ECF.

4. Limits of Finite Representation

In the AGM paradigm, the epistemic states of an agent are represented as theories which are in general infinite. However, according to Hansson [ 33, 34 ], the epistemic states of rational agents should have a finite representation. This is motivated from the perspective that epistemic states should resemble the cognitive states of human minds, and Hansson argues that as “finite beings”, humans cannot sustain epistemic states that do not have a finite representation. Further, finite representation is crucial from a computational perspective, to represent epistemic states in a computer.

Diferent strategies of finite representation have been used such as (i) finite bases [ 35, 36, 37 ], and (ii) finite sets of models [ 38, 39 ]. In the former strategy, each finite set of formulae, called a finite base , represents the theory Cn(). In the latter strategy, models are used to represent an epistemic state. Precisely, each finite set of models represents the theory of all formulae satisfied by all models in , that is, the theory { ∈ FmL | |= , for all ∈ }. The expressiveness of finite bases and finite sets of models are, in general (depending on the logic), incomparable, that is, some theories expressible in one method cannot be expressed in the other method and vice versa. For instance, the information that “John swims every two days” cannot be expressed via a finite base in LTL [ 40 ], although it can be expressed via a single Kripke structure (shown in Fig. 1, where stands for “John swims” ). On the other hand, “Anna will swim eventually” is expressible as a single LTL formula (F , where stands for “Anna swims” ), but it cannot be expressed via a finite set of models.

Given the incomparable expressiveness of these two wellestablished strategies of finite representations, it is not clear whether in general, and specifically in non-finitary logics, there exists a method capable of finitely representing all theories, therefore capturing the whole expressiveness of the logic. Towards answering this question, we provide a broad definition to conceptualise finite representation.

A finite representation for a theory can been seen as a ifnite word, i.e., a code, from a fixed finite alphabet Σ C. For example, the codes 1 := {a, b} and 2 := {a, a→b} are finite words in the language of set theory, and both represent the theory Cn({ ∧ }). The set of all codes, i.e., of all finite words over Σ C, is denoted by Σ *C. In this sense, a method of finite representation is a mapping from codes in Σ *C to theories. The pair (Σ C, ) is called an encoding. Definition 12 (Encoding). An encoding (Σ C, ) comprises a finite alphabet Σ C and a partial function : Σ *C ⇀ ThL.

Given an encoding (Σ C, ), a word ∈ Σ *C represents a theory , if () is defined and () = . Observe that a theory might have more than one code, whereas for others there might not exist a code. For instance, in the example above for finite bases, the codes 1 and 2 represent the same theory. On the other hand, recall that the LTL theory corresponding to “John swims every two days” cannot be expressed in the finite base encoding. Furthermore, the function is partial, because not all codes in Σ *C are meaningful. For instance, for the finite base encoding, the code {{}} cannot be interpreted as a finite base.

We are interested in logics which are AGM compliant, that is, logics in which rational contraction functions exist. Unfortunately, it is still an open problem how to construct AGM contraction functions in all such logics. The most general constructive apparatus up to date, as discussed in Section 3, are the Exhaustive Contraction functions proposed by Ribeiro et al. (2018) which assume only few conditions on the logic. Additionally, we focus on non-finitary logics, as the finitary case is trivial. We call such logics compendious. Definition 13 (Compendious Logics). A logic L is compendious if L is Tarskian, Boolean, non-finitary and satisfies: (Discerning) For all sets , ⊆ ⋂︀ = ⋂︀ implies = .

CCTL, we have that

Compendiousness amounts to expressivity in multiple dimensions. Compendious logics can express infinitely many distinct sentences (non-finitary), distinguish between a sentence being true or false (classical negation), and express uncertainty of two or more sentences (disjunction). The property (Discerning) is related the possible worlds semantics. In a possible world, the truth values of all sentences are known. From this perspective, possible worlds correspond to CCTs. Under the possible worlds semantics, an agent’s epistemic state is interpreted as the exact set of all possible worlds in which all the agent’s beliefs are true. If the truth value of a formula is unknown, the agent considers some possible worlds where is true, as well as possible worlds where is false. Hence, more possible worlds indicate strictly less information. Equivalently, diferent sets of possible worlds represent diferent epistemic states. This is exactly what (Discerning) conceptualises.

Example 14 (Discerning). Yara and Yasmin encounter a

large flightless bird. Yara knows that such birds exist in Africa and South America. Hence, Yara considers two possible worlds: the bird is from Africa (it is an ostrich), or the bird is from

South America (it is a rhea). Yasmin, who lived in Australia,

believes the bird is an emu (from Australia), a rhea or an ostrich. Since Yara and Yasmin consider diferent sets of possible worlds, their epistemic states difer. Yara believes in the disjunction ostrich ∨ rhea, Yasmin does not. She believes only in the disjunction ostrich ∨ rhea ∨ emu. As per (Discerning),

Yara and Yasmin present diferent epistemic states, due to the diference in the considered possible worlds.

The class of compendious logics is broad and includes several widely used logics.

Theorem 15. The logics LTL, CTL, CTL*, -calculus and

monadic second-order logic (MSO) are compendious.

It turns out that there is no method of finite representation capable of capturing all theories in a compendious logic.

Theorem 16. No encoding can represent every theory of a compendious logic.

Proof Sketch. We show that, since compendious logics are Tarskian, Boolean and non-finitary, there exist infinitely many CCTs. From (Discerning), it follows that there exist uncountably many theories in the logic. However, an encoding can represent only countably many theories.

As not every theory cann be finitely represented, only some subsets of theories can be used to express the epistemic states of an agent. We call a subset E of theories an excerpt of the logic. Each encoding induces an excerpt.

Definition 17.

The excerpt induced by an encoding (Σ C, )

is the set E := img( ). An excerpt induced by some encoding is called finitely representable .

5. The Büchi Encoding of LTL

The encoding in which epistemic states are expressed is of fundamental importance. On the one hand, the encoding must be expressive enough to capture a non-trivial space of epistemic states. On the other hand, the encoding must ∅,{} 0 ∅,{} 1 {} be able to decide whether it believes a given formula , i.e., whether is entailed by the theory representing the agent’s epistemic state. This question might be decidable for one (perhaps less expressive) encoding, but undecidable for a diferent (more expressive) encoding. We call this question the entailment problem on an encoding (Σ C, ): Input: (, ) ∈ Σ *C ×

FmL, such that () is defined Output: true if ∈ (), otherwise false

This problem is a generalisation of several decision problems that support reasoning. For example, on the finite base encoding, it corresponds to the usual entailment problem between formulae. Entailment on the encoding based on ifnite sets of models corresponds to the model checking problem. For other encodings, as we will see, it can be more general than either of these problems.

We investigate a suitable encoding for epistemic states over LTL, a commonly used compendious logic in model checking and planning. In both these domains, the primary approach to reason about LTL is based on Büchi automata. Thus, from a reasoning standpoint, Büchi automata are predestined to be the basis for an encoding of epistemic states over LTL. We give the following definition for the set of LTL formulae represented by a Büchi automaton: If ∈ (), we say that supports .

Definition 18 (Support). The support of a Büchi automaton

is the set () := { ∈ FmLTL | ∀ ∈ ℒ() . |= } negation ¬(G ) is not supported either.

Example 19. Figure 3 shows a Büchi automaton (on the

left), along with three supported formulae (on the right). All accepted traces satisfy these formulae. The formula G is not supported. While some accepted traces, such as {}, satisfy this formula, others, such as ∅ {} do not. Consequently, the

It remains to show that the support of a Büchi automaton is a theory. Perhaps surprisingly, the support of an arbitrary language of infinite traces (not represented as a Büchi automaton) does not necessarily form a theory. The disconnect arises from the fact that the semantics of LTL is defined over finite Kripke structures, and arbitrary languages of infinite traces can represent more fine-grained nuances of behaviours. Consider the language prime = {012 . . .}, where = {} if is a prime number and = ∅ otherwise. The support of prime prescribes that holds exactly in prime-numbered steps. Since no Kripke structure satisfies this requirement, the support of prime is inconsistent, yet prime does not support ⊥

An intriguing property of Büchi automata however is that their support is fully determined by those accepted traces that have the property of being ultimately periodic, that is, = for some finite sequences , . Recall from Section 2.2 that the superscript denotes infinite repetition of the subsequence . Ultimately periodic traces are tightly connected to CCTs: each CCT is satisfied by exactly one ultimately periodic trace. Let UP denote the set of all ultimately periodic traces. The correspondence between CCTs and ultimately periodic traces is formalized by the function ThUP : UP ThUP ( ) = { ∈ FmLTL | |= }.

Lemma 20. The function ThUP is a bijection.

→ CCTLTL such that

We combine Lemma 20 with two classical observations [ 11 ]: (i) every consistent LTL formula is satisfied by at least one ultimately periodic trace; and (ii) every Büchi automaton with nonempty language accepts some ultimately periodic trace. We arrive at the following characterization:

Lemma 21. The support of a Büchi automaton satisfies

() = ⋂︁ { ThUP ( ) | ∈ ℒ() ∩ UP } .

Theorem 22. The support of a Büchi automaton is a theory.

Thus, Büchi automata indeed define an encoding. Every Büchi automaton , being a finite structure, can be described in a finite code word , which the encoding maps to the theory (). We call this encoding the Büchi encoding, denoted (Σ Büchi, Büchi), and the induced excerpt the Büchi excerpt EBüchi. In terms of expressiveness, the Büchi excerpt strictly subsumes the classical approaches: Theorem 23. Let Ebase and Emodels denote respectively the excerpts of finite bases and finite sets of models 2. It holds that Ebase ∪ Emodels ⊊ E Büchi.

Proof Sketch. The expressiveness of the Büchi excerpt follows from Proposition 8. Figure 3 shows an automaton whose support can be expressed neither by a finite base nor a finite sets of models.

In terms of reasoning, the Büchi encoding benefits from the decidability properties of Büchi automata. Many decision problems, most importantly the entailment problem on the Büchi encoding, can be reduced to the decidable problem of inclusion between Büchi automata.

Theorem 24. The entailment problem on the Büchi encoding is decidable.

inclusion ℒ() ⊆ ℒ ( ).

Proof. Given a word ∈ Σ *Büchi that encodes a Büchi automaton , and an LTL formula , one can decide whether ∈ Büchi() = () by deciding the Büchi automata Beyond ensuring the decidability of key problems, an encoding’s suitability for reasoning also involves the question whether modifications of epistemic states can be realized by computations on code words. In particular in the context of the AGM paradigm, it is interesting to see if belief change operations can be performed in such a manner. The Büchi encoding also shines in this respect, since we can employ automata operations to this end. As a first example, consider the expansion of a theory with a formula . This operation corresponds to an intersection operation on Büchi automata, as the support of a Büchi automaton satisifes () +

= ( ⊓ ). The intersection automaton ⊓ can be computed through a product construction. 2These excerpts were described in the prologue of Section 4.

By contrast, the following two sections discuss fundamental limitations to efective constructions for rational contractions. Nevertheless, we show in Section 8 how the Büchi encoding admits similar automata-based constructions for a large subclass of contraction functions. 6. AGM

Accommodation

Assume that the space of epistemic states that an agent can entertain is determined by an excerpt E. In this section, we investigate which properties make an excerpt suitable from the AGM vantage point. Clearly, not every excerpt is suitable for representing the space of epistemic states. For example, if a non-tautological formula appears in each theory of E, then cannot be contracted. The chosen excerpt should be expressive enough to describe all relevant epistemic states that an agent might hold in response to its beliefs in flux. Precisely, if an agent is confronted with a piece of information and changes its epistemic state into a new one, then this new epistemic state must be expressible in the underlying excerpt. A straightforward option would be to require some sort of closure under AGM rationality, that is, all possible rational contractions involving information in the excerpt should be expressed yet within the excerpt. Such excerpts are closed under rational contraction resp. under fully rational contraction. We say that a contraction − remains in E if img(− ) ⊆ ways to contract . However, the finitely representable excerpt contains only countably many theories.

The negative result above concerns excerpts that are closed under rational contraction. As full rationality is strictly more demanding than rationality, one could hope to reach closedness by restricting to excerpts closed under fully rational contraction. Unfortunately, rationally closed excerpts and fully rationally closed excerpts coincide.

Proposition 27. An excerpt is closed under fully rational contraction if it is closed under rational contraction.

Instead of insisting on maximising the expressiveness of the excerpts, we impose a weaker condition and require the excerpt only to admit at least one rational outcome for each possible contraction.

Definition 28 (Accommodation). An excerpt E accommodates (fully) rational contraction if for each ∈ E there exists a (fully) rational contraction on that remains in E.

Accommodation guarantees that an agent can modify its beliefs rationally, in all possible epistemic states covered by the excerpt. There is a clear connection between accommodation and AGM compliance. While AGM compliance concerns existence of rational contraction operations in every theory of a logic, accommodation guarantees that the information in each theory within the excerpt can be rationally contracted and that its outcome can yet be expressed within the excerpt. Analogous to closedness, rational accommodation and fully rational accommodation coincide. Proposition 29. An excerpt E accommodates rational contraction if E accommodates fully rational contraction.

7. Uncomputability of Contraction

Accommodation is the weakest condition we can impose upon an excerpt to guarantee the existence of AGM rational contractions. Yet, the existence of contractions does not imply that an agent can efectively contract information. Thus we investigate the question of computability of contraction functions. For this endeavor, the focus on contraction functions that remain in the excerpt is crucial: both input and output of a computation must be finitely representable. We thus fix a finitely representable excerpt E that accommodates contraction. As an agent has to reason about its beliefs, it should be able to decide whether two formulae are logically equivalent. Hence, we assume that, in the underlying logic, logical equivalence is decidable.

Definition 3. 0 (AGM Computability). Let be a theory in E, and let − be a. contraction function on that remains in E. We say that − is computable if there exists an encoding (Σ C, ) that induces E, such that the following problem is computed by a Turing machine: Input: A formula ∈ FmL. .

Output: A word ∈ Σ *C such that () = − .

In the classical setting of finitary logics, computability of AGM contraction is trivial, as there are only finitely many formulae (up to equivalence), and only a finite number of theories. By contrast, compendious logics have infinitely many formulae (up to equivalence) and consequently inifnitely many theories.

In the following, unless otherwise stated, we only consider compendious logics. In such logics, we distinguish two kinds of theories: those that contain infinitely many formulae (up to equivalence), and those that contain only ifnitely many formulae (up to equivalence). An excerpt that constrains an agent’s epistemic states to the latter case essentially disposes of the expressive power of the compendious logic, as in each epistemic state only finitely many sentences can be distinguished. Therefore, such epistemic states could be expressed in a finitary logic. As the computability in the finitary case is trivial, we focus on the more expressive case.

Definition 31 (Non-Finitary). A theory is non-finitary if it contains infinitely many logical equivalence classes of formulae.

Note that being non-finitary is a very general condition. Even theories with a finite base can be non-finitary. For instance, the LTL theory Cn(G ) contains the infinitely many non-equivalent formulae {, X , X2 , X3 , . . .}.

In the remainder of this section, we establish a strong link between non-finitary theories and uncomputable contraction functions. To this end, we introduce the notion of cleavings.

Definition 32 (Cleaving). A cleaving is an infinite set of

formulae such that for all two distinct , ∈ we have: (CL1) and are not equivalent ( ̸≡ ); and (CL2) the disjunction ∨ is a tautology.

From an algebraic perspective, the formulae in a cleaving behave like a kind of weak complement: we require that the disjunction ∨ is a tautology, whereas we do not require the conjunction ∧ to be inconsistent (as would be the case for the conjunction ∧ ¬ ).

Example 33. Consider the logic of elementary arithmetic

over natural numbers. The formulae ̸= 0, ̸= 1, ̸= 2, etc. form a cleaving: they are pairwise non-equivalent, and every disjunction ( ̸= ) ∨ ( ̸= ) is a tautology (where , are two diferent constants).

Example 34. Let twice() :≡ F ( ∧ X F ) be the LTL formula denoting that proposition holds at least twice, and for ∈ N, let :≡ (X ) → twice() be the formula stating that if holds in time step , it must hold at least one additional time (i.e., at least twice overall). For ̸= , the formulae and are non-equivalent. Further, the disjunction ∨ simplifies to (X )∧(X ) → twice().

The latter formula is a tautology: if holds in time steps

and , it holds at least twice. Hence, the set of formulae { 0, 1, . . .} is a cleaving.

Lemma 35. Every non-finitary theory contains a cleaving.

Given a contraction that remains in an excerpt, cleavings provide a way of generating many diferent contractions that remain within the excerpt. This works by ranking the formulae in the cleaving such that each rank has exactly one formula. We reduce the contraction of a formula to contracting ∨ , where is the lowest ranked formula in the cleaving such that ∨ is non-tautological. Each new contraction depends on the original choice function and the ranking.

Definition 36 (Composition). Let be a choice function on a theory , ⊆ be a cleaving, and : N → be a permutation of . The composition of and is the function : Fm → (CCT) such that

( ) := (︀ ∨ min ( )︀) where min ( ) = (), for the minimal ∈ N such that ∨ () ̸≡ ⊤ , or min ( ) = ⊥ if no such exists. Example 37. Consider the cleaving { 0, 1, . . .} of Example 34, and let be the permutation with () = for all ∈ N. The formula ∨ 0 is a tautology. Thus, we have min () = (1) = 1 and the choice function chooses () = ( ∨ 1). If we however consider a permutation ′ with ′(0) = 2 and ′(2) = 0, then we have min ′ () = ′(0) = 2 and ′ () = ( ∨ 2).

If we consider the formula F G ¬ stating that only holds ifnitely often, any disjunction of the form (F G ¬) ∨ is a tautology: either there are only finitely many occurrences of , or otherwise, holds infinitely often, and so holds at least twice. Hence, we have, for both permutations, (F G ¬) = ′ (F G ¬) = (︀ (F G ¬) ∨ ⊥︀) = (F G ¬).

The composition of a choice function with a permutation of a cleaving preserves rationality.

Lemma 38. The composition of a choice function and

a permutation : N → of a cleaving ⊆ is a choice function.

A composition generates a new choice function which in turn induces a rational contraction function that remains within the excerpt. Yet, the induced contraction function is not necessarily computable.

Theorem 39. Let E accommodate rational contraction, and let ∈ E. The following statements are equivalent: 1. The theory is non-finitary.

2. There exists an uncomputable rational contraction

function on that remains in E.

3. There exists an uncomputable fully rational contrac

tion function on that remains in E.

Proof Sketch. Let be non-finitary, and the choice function of a (fully) rational contraction for that remains in E. Each permutation of a cleaving ⊆ induces a distinct (fully) rational contraction (with choice function ) that remains in E. At most countably many of these uncountably many (fully) rational contractions can be computable.

If is finitary, every contraction function is computable, as it only has to consider finitely many formulae.

Theorem 39 makes evident that uncomputability of AGM contraction is inevitable. In fact, there are uncountably many uncomputable contraction functions. The only way to avoid this uncomputability would be to restrain the expressiveness of the excerpt to the most trivial case: only ifnitary theories.

8. Efective Contraction in the Büchi

Excerpt

Despite the strong negative result of Section 7, computability can still be harnessed in very particular excerpts: excerpts E in which for every theory, there exists at least one computable (fully) rational contraction function that remains in E. We say that such an excerpt E efectively accommodates (fully) rational contraction. If belief contraction is to be computed for compendious logics, it is paramount to identify such excerpts as well as classes of computable contraction functions. In this section, we show that the Büchi excerpt of LTL efectively accommodates (fully) rational contraction.

For a contraction on a theory ∈ EBüchi to remain in the Büchi excerpt, the underlying choice function must be ¬G F : (G F ): designed such that the intersection of with the selected CCTs corresponds to the support of a Büchi automaton. As CCTs and ultimately periodic traces are interchangeable (Lemma 20), and the support of a Büchi automaton is determined by the CCTs corresponding to its accepted ultimately periodic traces (Lemma 21), a solution is to design a selection mechanism, analogous to choice functions, that picks a single Büchi automaton instead of an (infinite) set of CCTs. Definition 40 (Büchi Choice Functions). A Büchi choice function maps each LTL formula to a single Büchi automaton, such that for all LTL formulae and , (BF1) the language accepted by ( ) is non-empty; (BF2) ( ) supports ¬ , if is not a tautology; and (BF3) ( ) and ( ) accept the same language, if ≡ .

Conditions (BF1) - (BF3) correspond to the respective conditions (CF1) - (CF3) in the definition of choice functions. Each Büchi choice function induces a contraction function. Definition 41 (Büchi Contraction Functions). Let be a theory in the Büchi excerpt and let be a Büchi choice function. The Büchi Contraction Function (BCF) on induced by is the function

. − = {︃ ∩ ( ( )) if /∈ Cn(∅) and ∈

otherwise

All such contractions remain in the Büchi excerpt. Indeed, one can observe that if = () for a Büchi automaton , it holds that ∩ ( ( )) = ( ⊔ ( )). Recall from Section 2 that ⊔ denotes the union of Büchi automata. The class of all rational contraction functions that remain in the Büchi excerpt corresponds exactly to the class of all BCFs. .

Theorem 42. A contraction function − on a theory ∈ EBüchi is r.ational and remains within the Büchi excerpt if and only if − is a BCF.

Example 43. Let = (), for the Büchi automaton shown in Fig. 3. To contract the formula G F , a Büchi choice function may select the Büchi automaton (G F ) shown in Fig. 4. This automaton supports ¬G F ; the automaton ¬G F is shown for reference. In fact, (G F ) accepts precisely the traces satisfying ∧ ¬G F . The result of the contraction is the theory () ∩ ( (G F )), which corresponds to the theory ( ⊔ (G F )), whose supporting automaton is also shown in Fig. 4. The union ⊔ is obtained by simply taking the union of states and transitions.

This automaton does not support G F , and therefore the contraction is successful.

As BCFs capture all rational contractions within the excerpt, it follows from Theorem 39 that not all BCFs are computable. Note from Definition 41 that to achieve computability, it sufices to be able to: (i) decide if is a tautology, (ii) decide if ∈ , (iii) compute the underlying Büchi choice function , and (iv) compute the intersection of with the support of ( ). We already know that conditions (i) and (ii) are satisfied (Theorem 24). For condition (iv), recall that the intersection of the support of two automata is equivalent to the support of their union. As produces a Büchi automaton, and union of Büchi automata is computable, condition (iv) is also satisfied. Therefore, condition (iii) is the only one remaining. It turns out that (iii) is a necessary and suficient condition to characterize all computable contraction functions within the Büchi excerpt.

.

Theorem 44. Let − be a ration.al contraction function on a theory ∈ EBüchi, .such that − remain.s in th.e Büchi excerpt. The operation − is computable if − = − for some computable Büchi choice function .

Note that there do indeed exist computable choice functions. As an example, the full meet contraction [ 1, 3 ] is computable. The corresponding Büchi choice function fm is given by fm( ) = ¬ if is non-tautological, and fm( ) = ⊤ otherwise. This function is computable: the automata ¬ and ⊤ can be efectively constructed, and it is decidable whether the given LTL formula is a tautology.

As the full meet contraction is fully rational, we conclude that the Büchi excerpt efectively accommodates (fully) rational contraction.

9. Conclusion

We have investigated the computability of AGM contraction for the class of compendious logics, which embrace several logics used in computer science and AI. Due to the high expressive power of these logics, not all epistemic states admit a finite representation. Hence, the epistemic states that an agent can assume are confined to a space of theories, which depends on a method of finite representation. We have shown a severe negative result: no matter which form of finite representation we use, as long as it does not collapse to the finitary case, AGM contraction sufers from uncomputability. Precisely, there are uncountably many uncomputable (fully) rational contraction functions in all such expressive spaces. This negative result also impacts other forms of belief change. For instance, belief revision is interdefinable with belief contraction, via the Levi Identity. Therefore, it is likely that revision also sufers from uncomputability. Accordingly, uncomputability might span to iterated belief revision [ 41 ], update and erasure [ 42 ], and pseudo-contraction [ 43 ], to cite a few. It is worth investigating uncomputability of these other operators.

In this work, we have focused on the AGM paradigm, and logics which are Boolean. We intend to expand our results for a wider class of logics by dispensing with the Boolean operators, and assuming only that the logic is AGM compliant. We believe the results shall hold in the more general case, as our negative results follow from cardinality arguments. On the other hand, several logics used in knowledge representation and reasoning are not AGM compliant, as for instance a variety of Description Logics [ 12 ]. In these logics, the recovery postulate (K−5 ) can be replaced by the relevance postulate [ 44 ], and contraction functions can be properly defined. Such logics are called relevancecompliant. As relevance is an weakened version of recovery, the uncomputability results in this work translate to various relevance-compliant logics. However, it is unclear if all such logics are afected by uncomputability. We aim to investigate this issue in such logics.

Even if we have to coexist with uncomputability, we can still identify classes of operators which are guaranteed to be computable. To this end, we have introduced a novel class of contraction functions for LTL using Büchi automata, and identified the conditions needed for computability. This is an initial step towards the application of belief change in other areas, such as methods for automatically repairing systems [ 45 ]. The methods devised here for LTL form a foundation for the development of analogous strategies for other expressive logics, such as CTL, -calculus and many Description Logics. For example, in these logics, similarly to LTL, decision problems such as satisfiability and entailment have been solved using various kinds of automata, such as tree automata [ 46, 47 ].

References

[1] C. E. Alchourrón , P. Gärdenfors , D. Makinson , On the logic of theory change: Partial meet contraction and revision functions , J. Symb. Log . 50 ( 1985 ) 510 - 530 . doi: 10 .2307/2274239.

[2] P. Gärdenfors , Knowledge in flux: Modeling the dynamics of epistemic states ., The MIT press, 1988 .

[3] S. O. Hansson , A textbook of belief dynamics - theory change and database updating , volume 11 of Applied logic series, Kluwer, 1999 .

[4] C. E. Alchourrón , D. Makinson , On the logic of theory change: Contraction functions and their associated revision functions , Theoria 48 ( 1982 ) 14 - 37 . doi: 10 . 1111/j.1755- 2567 . 1982 .tb00480.x.

[5] P. Gärdenfors , An epistemic approach to conditionals , American Philosophical Quarterly 18 ( 1981 ) 203 - 211 .

[6] S. O. Hansson , Kernel contraction, J. Symb. Log . 59 ( 1994 ) 845 - 859 . doi: 10 .2307/2275912.

[7] A. Grove , Two modellings for theory change , J. Philos. Log . 17 ( 1988 ) 157 - 170 . doi: 10 .1007/BF00247909.

[8] G. Flouris , On Belief Change and Ontology Evolution, Ph.D. thesis , University of Crete, 2006 .

[9] F. Baader , I. Horrocks, C. Lutz , U. Sattler , An Introduction to Description Logic, Cambridge University Press, 2017 .

[10] P. Blackburn , J. F. A. K. van Benthem , F. Wolter (Eds.), Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning , North-Holland, 2007 .

[11] E. M. Clarke , O. Grumberg , D. Kroening , D. A. Peled , H. Veith , Model checking, 2nd Edition , MIT Press, 2018 .

[12] M. M. Ribeiro , R. Wassermann , G. Flouris, G. Antoniou, Minimal change: Relevance and recovery revisited , Artif. Intell . 201 ( 2013 ) 59 - 80 . doi: 10 .1016/J.ARTINT. 2013 . 06 .001.

[13] J. P. Delgrande , P. Peppas , Belief revision in Horn theories , Artif. Intell . 218 ( 2015 ) 1 - 22 . doi: 10 .1016/ J.ARTINT. 2014 . 08 .006.

[14] J. P. Delgrande , R. Wassermann , Horn clause contraction functions: Belief set and belief base approaches , in: KR, AAAI Press, 2010 .

[15] R. Booth , T. Meyer, I. Varzinczak, R. Wassermann , On the link between partial meet, kernel, and infra contraction and its application to Horn logic , CoRR abs/1401 .3902 ( 2014 ). arXiv: 1401 . 3902 .

[16] N. C. da Costa , O. Bueno , Belief change and inconsistency , Logique et Analyse 41 ( 1998 ) 31 - 56 .

[17] M. M. Ribeiro , R. Wassermann , Base revision for ontology debugging , J. Log. Comput . 19 ( 2009 ) 721 - 743 . doi: 10 .1093/LOGCOM/EXN048.

[18] J. S. Ribeiro , A. Nayak , R. Wassermann , Towards belief contraction without compactness , in: KR, AAAI Press, 2018 , pp. 287 - 296 .

[19] R. Wassermann , On AGM for non-classical logics , J. Philos. Log . 40 ( 2011 ) 271 - 294 . doi: 10 .1007/ S10992-011-9178-2.

[20] B. Nebel , How Hard is it to Revise a Belief Base?, Springer Netherlands, 1998 , pp. 77 - 145 .

[21] T. Eiter , G. Gottlob, On the complexity of propositional knowledge base revision, updates, and counterfactuals , Artif. Intell . 57 ( 1992 ) 227 - 270 . doi: 10 .1016/ 0004 - 3702 ( 92 ) 90018 - S .

[22] N. Schwind , S. Konieczny , J. Lagniez , P. Marquis , On computational aspects of iterated belief change, in: IJCAI, ijcai .org, 2020 , pp. 1770 - 1776 . doi: 10 .24963/ IJCAI. 2020 /245.

[23] J. Richard Büchi , Symposium on Decision Problems: On a Decision Method in Restricted Second Order Arithmetic , volume 44 of Studies in Logic and the Foundations of Mathematics, Elsevier , 1966 , pp. 1 - 11 . doi: 10 .1016/ S0049 -237X( 09 ) 70564 - 6 .

[24] W. M. P. van der Aalst , M. Pesic, H. Schonenberg , Declarative workflows: Balancing between flexibility and support , Comput. Sci. Res . Dev. 23 ( 2009 ) 99 - 113 . doi: 10 .1007/S00450-009-0057-9.

[25] S. Cerrito , M. C. Mayer , Bounded model search in linear temporal logic and its application to planning , in: TABLEAUX, volume 1397 of Lecture Notes in Computer Science, Springer, 1998 , pp. 124 - 140 . doi: 10 .1007/ 3-540-69778-0\_ 18 .

[26] G. D. Giacomo , M. Y. Vardi , Automata-theoretic approach to planning for temporally extended goals , in: ECP , volume 1809 of Lecture Notes in Computer Science , Springer, 1999 , pp. 226 - 238 . doi: 10 .1007/ 10720246\_ 18 .

[27] V. Gutiérrez-Basulto , J. C. Jung , A. Ozaki , On metric temporal description logics , in: ECAI , volume 285 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2016 , pp. 837 - 845 . doi: 10 .3233/ 978-1- 61499 -672-9-837.

[28] V. Gutiérrez-Basulto , J. C. Jung , T. Schneider , Lightweight temporal description logics with rigid roles and restricted TBoxes , in: IJCAI, AAAI Press, 2015 , pp. 3015 - 3021 .

[29] D. Klumpp , J. S. Ribeiro , Walking the Tightrope between Expressiveness and Uncomputability: AGM Contraction beyond the Finitary Realm (Extended Version) , Technical Report , 2024 . URL: https://dominik-klumpp.net/publications/nmr24/ extended.pdf.

[30] F. Patrizi , N. Lipovetzky , G. D. Giacomo , H. Gefner , Computing infinite plans for LTL goals using a classical planner , in: IJCAI, IJCAI/AAAI , 2011 , pp. 2003 - 2008 . doi: 10 .5591/978-1- 57735 -516-8/ IJCAI11 -334.

[31] E. L. Fermé , S. O. Hansson , Belief Change - Introduction and Overview , Springer Briefs in Intelligent Systems, Springer, 2018 . doi: 10 .1007/ 978-3- 319 -60535-7.

[32] J. S. Ribeiro , A. Nayak , R. Wassermann , Belief change and non-monotonic reasoning sans compactness , in: AAAI, AAAI Press, 2019 , pp. 3019 - 3026 . doi: 10 .1609/ AAAI.V33I01.33013019.

[33] S. O. Hansson , Descriptor Revision: Belief Change Through Direct Choice , volume 46 , Springer, 2017 .

[34] S. O. Hansson , Finite contractions on infinite belief sets , Stud Logica 100 ( 2012 ) 907 - 920 . doi: 10 .1007/ S11225-012-9440-9.

[35] B. Nebel , Reasoning and Revision in Hybrid Representation Systems , volume 422 of Lecture Notes in Computer Science, Springer, 1990 . doi: 10 .1007/ BFB0016445.

[36] M. Dalal , Investigations into a theory of knowledge base revision , in: AAAI, AAAI Press / The MIT Press, 1988 , pp. 475 - 479 .

[37] S. E. Dixon , Belief revision: A computational approach , Ph.D. thesis , University of Sydney, 1994 .

[38] H. van Ditmarsch , W. van Der Hoek , B. Kooi , Dynamic epistemic logic , volume 337 , Springer Science & Business Media , 2007 .

[39] A. Baltag , L. S. Moss , S. Solecki, The logic of public announcements and common knowledge and private suspicions , in: TARK, Morgan Kaufmann, 1998 , pp. 43 - 56 .

[40] P. Wolper , Temporal logic can be more expressive , Inf. Control . 56 ( 1983 ) 72 - 99 . doi: 10 .1016/ S0019- 9958 ( 83 ) 80051 - 5 .

[41] A. Darwiche , J. Pearl , On the logic of iterated belief revision , Artif. Intell . 89 ( 1997 ) 1 - 29 . doi: 10 .1016/ S0004- 3702 ( 96 ) 00038 - 0 .

[42] H. Katsuno , A. O. Mendelzon , On the diference between updating a knowledge base and revising it , in: P. Gärdenfors (Ed.), Belief revision, 2003 , pp. 183 - 203 .

[43] S. O. Hansson , Changes of disjunctively closed bases , J. Log. Lang. Inf . 2 ( 1993 ) 255 - 284 . doi: 10 .1007/ BF01181682.

[44] S. O. Hansson , Belief contraction without recovery , Stud Logica 50 ( 1991 ) 251 - 260 . doi: 10 .1007/ BF00370186.

[45] P. T. Guerra , R. Wassermann , Two AGM-style characterizations of model repair , in: KR, AAAI Press, 2018 , pp. 645 - 646 .

[46] O. Kupferman , M. Y. Vardi , P. Wolper , An automatatheoretic approach to branching-time model checking , J. ACM 47 ( 2000 ) 312 - 360 . doi: 10 .1145/333979. 333987.

[47] J. Hladik , R. Peñaloza , PSPACE automata for description logics , in: Description Logics , volume 189 of CEUR Workshop Proceedings, CEUR-WS.org , 2006 .