Walking the Tightrope between Expressiveness and Uncomputability: AGM Contraction beyond the Finitary Realm Dominik Klumpp1,* , Jandson S Ribeiro2 1 University of Freiburg, Germany 2 Cardiff University, United Kingdom 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 para-consistent logics [16], Description Logics [17, 12, 8], and non-compact logics [18]. See [19] for a discussion of The field of Belief Change [1, 2, 3] investigates how to keep a several other works in this line. corpus of beliefs consistent as it evolves. The field is mainly Although much effort has been put into extending the founded on the AGM paradigm [1], named after its authors’ AGM paradigm to more expressive logics, few works have in- initials, which distinguishes, among others, two main kinds vestigated the computational aspects of the AGM paradigm of changes: belief revision, which consists in incorporating such as [20, 21, 22]. All these works, however, focused on an incoming piece of information with the proviso that the investigating the complexity of decision problems for some updated corpus of beliefs is consistent; and belief contraction fixed belief change operators on classical propositional log- whose purpose is to retract an obsolete piece of information. ics and Horn. In light of the interest and effort of expanding In either case, the incurred changes should be minimized the AGM paradigm for more expressive non-classical logics, so that most of the original beliefs are preserved. This is it is paramount to comprehend the computational aspects of known as principle of minimal change. Contraction is central belief change in such more expressive logics. In this context, as it can be used to define other forms of belief change. For there is a central question that even precedes complexity: example, belief revision can be defined in terms of contrac- tion: first, remove information in conflict with the incoming Computability / Effectiveness: Given a belief change belief via contraction, only then incorporate the incoming operator ∘, does there exist a Turing Machine that belief. When classical negation is at disposal, this recipe for computes ∘, and stops on all inputs? defining revision from contraction is formalised via the Levi identity [4, 5]. The answer to the question above depends on two main The AGM paradigm prescribes rationality postulates that elements: the underlying logic, and the chosen operator. capture the principle of minimal change, and constructive Clearly, it only makes sense to answer such questions for functions that satisfy such postulates, called rational func- logics that are AGM compliant. However, independently tions, as for instance partial meet [1], (smooth) kernel con- of the operator, the question is trivial for finitary logics, traction [6], epistemic entrenchment [2] and Grove’s system that is, logics whose language contains only finitely many of spheres [7]. Originally, the AGM paradigm was developed equivalence classes, as it is the case of classical propositional assuming some conditions about the underlying logic [2, 8]. logics. For non-finitary logics, by contrast, we show a dis- Although these conditions cover some classical logics such ruptive result: AGM rational contraction functions suffer as classical Propositional Logic and First Order Logic, they from uncomputability. restrict the reach of the AGM paradigm into more expres- This first result uses all the expressive power of the un- sive logics including several Descriptions Logics [9], Modal derlying logic. To control computability, one could limit Logics [10] and Temporal Logics such as LTL, CTL and CTL* the space of epistemic states to some specific set of theories [11]. It turns out that the AGM paradigm is independent of (logically closed set of sentences). However, we show that such conditions [8], although rational contraction functions no matter how much we constrain the space of epistemic do not exist in every logic [8, 12]. Logics in which rational states, uncomputability still remains, as long as the restric- contraction functions do exist are dubbed AGM compliant tion is not so severe that the space collapses back to the [8]. As a result, several works have been dedicated to dis- finitary case. Although this shows that uncomputability is pense with the AGM assumptions in order to extend the unavoidable in all such expressive spaces, it is of extreme paradigm to more expressive logics: Horn logics [13, 14, 15], importance to identify how, and under which conditions, one can construct specific (families of) contraction func- tions that are computable. We investigate this question for 22nd International Workshop on Nonmonotonic Reasoning, November 2-4, 2024, Hanoi, Vietnam Linear Temporal Logic (LTL), and we show that when rep- * Corresponding author. resenting epistemic states via Büchi automata [23], we can $ klumpp@informatik.uni-freiburg.de (D. Klumpp); construct families of contraction functions that are com- ribeiroj@cardiff.ac.uk (J. S. Ribeiro) putable within such a space. LTL is a very expressive logic € https://dominik-klumpp.net/ (D. Klumpp); used in a plethora of applications in Computer Science and https://jandsonribeiro.github.io/home/ (J. S. Ribeiro)  0000-0003-4885-0728 (D. Klumpp); 0000-0003-1614-6808 AI. For example, LTL has been used for specification and (J. S. Ribeiro) verification of software and hardware systems [11], in busi- © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). ness process models such as DECLARE [24], in planning and CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings reasoning about actions [25, 26], and extending Description ℓ1 ℓ0 ℓ2 Logics with temporal knowledge [27, 28]. Büchi automata {} {𝑝} {𝑝} are endued with closure properties which allow for both effective reasoning and computable contraction functions. Figure 1: A Kripke structure on AP = {𝑝}, with an initial Roadmap: In Section 2, we review basic concepts regard- state ℓ0 . The labels 𝜆(ℓ𝑖 ) are shown below each state ℓ𝑖 . ing 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, We omit subscripts whenever the meaning is clear. 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 com- 2.1. Linear Temporal Logic pendious logics, not all epistemic states can be represented We recall the definition of linear temporal logic [11], LTL for finitely. In Section 5, we present an expressive method of short. For the remainder of the paper, we fix an arbitrary finite representation for LTL which is based on Büchi au- finite, nonempty set AP of atomic propositions. tomata, and discuss how it supports reasoning. Section 6 introduces the notion of AGM closedness, i.e., every rational Definition 1 (LTL Formulae). Let 𝑝 range over AP . The contraction outcome on a finitely representable belief state formulae of LTL are generated by the following grammar: should again be finitely representable. We show that, under certain weak conditions, closedness cannot be satisfied for 𝜙 ::= ⊥ | 𝑝 | ¬𝜙 | 𝜙 ∨ 𝜙 | X 𝜙 | 𝜙 U 𝜙 compendious logics. In Section 7, we establish our third negative result for compendious logics: even if we restrict Fm LTL denotes the set of all LTL formulae. ourselves to contraction functions whose output can be rep- In LTL, time is interpreted as a linear timeline that unfolds resented, uncomputability of contraction is inevitable in the infinitely into the future. The operator X states that a non-finitary case, i.e., there always exist uncountably many formula holds in the next time step, while 𝜙 U 𝜓 means uncomputable contraction functions. On the positive side, that 𝜙 holds until 𝜓 holds (and 𝜓 does eventually hold). We in Section 8, we show that computable contractions do exist define the usual abbreviations for boolean operations (⊤, ∧, for LTL theories represented via Büchi automata, and we →) as well as the temporal operators F 𝜙 := ⊤ U 𝜙 (finally, identify the conditions needed for computability. Section 9 at some point in the future), G 𝜙 := ¬F ¬𝜙 (globally, at all discusses the impact of our results and provides an outlook points in the future), and X𝑘 𝜙 for repeated application of on future work. X , where 𝑘 ∈ N. A version of the paper including proofs is available [29]. Formally, timelines are modelled as traces. A trace is an infinite sequence 𝜋 = 𝑎0 𝑎1 . . ., where each 𝑎𝑖 ∈ 𝒫(AP ) 2. Logics and Automata is a set of atomic propositions that hold at time step 𝑖. The infinite suffix of 𝜋 starting at time step 𝑖 is denoted by 𝜋 𝑖 = We review a general notion of logics that will be used 𝑎𝑖 𝑎𝑖+𝑖 · · · . The set of all traces is denoted by 𝒫(AP )𝜔 . throughout the paper. We use 𝒫(𝑋) to denote the power The semantics of LTL is defined in terms of Kripke struc- set of a set 𝑋. A logic is a pair L = (Fm, Cn) comprising a tures [11], which describe possible traces. countable1 set of formulae Fm, and a consequence operator Definition 2 (Kripke Structure). A Kripke structure is a Cn : 𝒫(Fm) → 𝒫(Fm) that maps each set of formulae to tuple 𝑀 = (𝑆, 𝐼, 𝑇, 𝜆) such that 𝑆 is a finite set of states; the conclusions entailed from it. We sometimes write Fm L 𝐼 ⊆ 𝑆 is a non-empty set of initial states; 𝑇 ⊆ 𝑆 × 𝑆 is and Cn L for brevity. a left-total transition relation, i.e., for all 𝑠 ∈ 𝑆 there exists We consider logics that are Tarskian, that is, logics whose 𝑠′ ∈ 𝑆 such that (𝑠, 𝑠′ ) ∈ 𝑇 ; and 𝜆 : 𝑆 → 𝒫(AP ) labels consequence operator Cn is monotone (if 𝑋1 ⊆ 𝑋2 then states with sets of atomic propositions. Cn(𝑋1 ) ⊆ Cn(𝑋2 )), extensive (𝑋 ⊆ Cn(𝑋)) and idempo- tent (Cn(Cn(𝑋)) = Cn(𝑋)). We say that two formulae A trace of a Kripke structure 𝑀 is a sequence 𝜙, 𝜓 ∈ Fm are logically equivalent, denoted 𝜙 ≡ 𝜓, if 𝜋 = 𝜆(𝑠0 )𝜆(𝑠1 )𝜆(𝑠2 ) . . . with 𝑠0 ∈ 𝐼, and for all 𝑖 ≥ 0, Cn(𝜙) = Cn(𝜓). Cn(∅) is the set of all tautologies. A 𝑠𝑖 ∈ 𝑆 and (𝑠𝑖 , 𝑠𝑖+1 ) ∈ 𝑇 . The set of all traces from a theory of L is a set of formulae 𝒦 such that Cn(𝒦) = 𝒦. Kripke structure 𝑀 is given by Traces(𝑀 ). Figure 1 shows The expansion of a theory 𝒦 by a formula 𝜙 is the theory an example of a Kripke structure, in graphical notation. 𝒦 + 𝜙 := Cn(𝒦 ∪ {𝜙}). Let ThL denote the set of all theo- The satisfaction relation between Kripke structure and ries of L. If ThL is finite, we say that L is finitary; otherwise, LTL formulae is defined in terms of the satisfaction between L is non-finitary. Equivalently, L is finitary if L has only the Kripke structure’s traces and LTL formulae. finitely many formulae up to logical equivalence. A theory 𝒦 is consistent if 𝒦 ̸= Fm, and it is complete if Definition 3 (Satisfaction). The satisfaction relation be- for all formulae 𝜙 ∈ / 𝒦, we have 𝒦 + 𝜙 = Fm. The set of tween traces and LTL formulae is the least relation |= ⊆ all complete consistent theories of L is denoted as CCTL . 𝒫(AP )𝜔 × Fm LTL such that, for all traces 𝜋 = 𝑎0 𝑎1 . . . ∈ The set of all CCTs that do not contain 𝜙 is given by 𝜔(𝜙). 𝒫(AP )𝜔 : A logic L is Boolean, if Fm L 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 𝜋 |= 𝑝 iff 𝑝 ∈ 𝑎0 𝒦 ∈ ThL to coincide with the 𝜋 |= ¬𝜙 iff 𝜋 ̸|= 𝜙 ⋂︀ intersection of all the CCTs 𝜋 |= 𝜙1 ∨ 𝜙2 iff 𝜋 |= 𝜙1 or 𝜋 |= 𝜙2 containing 𝒦, that is, 𝒦 = { 𝒦′ ∈ CCTL | 𝒦 ⊆ 𝒦′ }. 𝜋 |= X 𝜙 iff 𝜋 1 |= 𝜙 1 A set 𝑋 is countable if there is an injection from 𝑋 to the natural 𝜋 |= 𝜙1 U 𝜙2 iff there exists 𝑖 ≥ 0 s.t. 𝜋 𝑖 |= 𝜙2 numbers. and for all 𝑗 < 𝑖, 𝜋 𝑗 |= 𝜙1 Büchi automaton 𝐴𝒦 : Some Infinite Words from ℒ(𝐴𝒦 ): 𝑥 where each arrow 𝑞 → 𝑞 ′ indicates the transition (𝑞, 𝑥, 𝑞 ′ ) in ∅,{𝑝} 𝜔 the automaton. By concatenating the letters in this sequence, 𝜋1 = ∅ ∅ ∅ {𝑝} (∅ {𝑝}) {𝑝} 𝜔 we get the infinite word 𝜋1 defined in Figure 2. The acceptance ∅,{𝑝} 𝜋2 = {𝑝} {𝑝} ∅ (∅ {𝑝}) 𝑞0 𝑞1 𝑞2 𝜔 condition requires some recurrence states to appear infinitely 𝜋3 = {𝑝} {𝑝} ∅ {𝑝} ∅, {𝑝} often. As for instance the recurrence state 𝑞1 appears infinitely often, the acceptance condition holds and 𝜋1 is accepted. Anal- Figure 2: A Büchi automaton (on the right), and some infinite ogously, the infinite words 𝜋2 and 𝜋3 are also accepted. words accepted by this automaton (on the left). On the other hand, the infinite word 𝜋 ′ = ∅𝜔 is not ac- cepted, as the only sequence of states that produces this word is ∅ ∅ ∅ 𝑞0 → 𝑞0 → 𝑞0 . . ., where 𝑞0 → loops. The only state in this A Kripke structure 𝑀 satisfies a formula 𝜙, denoted sequence is 𝑞0 which is not a recurrence state and, therefore, 𝑀 |= 𝜙, iff all traces of 𝑀 satisfy 𝜙. 𝑀 satisfies a set 𝑋 the acceptance condition is violated. of formulae, 𝑀 |= 𝑋, iff 𝑀 |= 𝜙 for all 𝜙 ∈ 𝑋. The con- Emptiness of a Büchi automaton’s language is decidable. sequence operator Cn LTL is defined from the satisfaction Further, Büchi automata for the union, intersection and relation. complement of the languages of given Büchi automata can Definition 4 (Consequence Operator). The consequence be effectively constructed [23]. In the remainder of the operator Cn LTL maps each set 𝑋 of LTL formulae to the set paper we specifically make use of the construction for union of all formulae 𝜓, such that for all Kripke structures 𝑀 , if and intersection, and denote them with the symbol ⊔ resp. 𝑀 |= 𝑋 then also 𝑀 |= 𝜓. ⊓. The automata-theoretic treatment for several crucial reasoning problems in LTL, such as model-checking and Observation 5. LTL is Tarskian and Boolean. satisfiability, is based on the following result: Proposition 8 ([11]). For every LTL formula 𝜙 and every 2.2. Büchi Automata Kripke structure 𝑀 , there exist Büchi automata 𝐴𝜙 and 𝐴𝑀 Büchi automata are finite automata widely used in formal that accept precisely the traces that satisfy 𝜙 resp. the traces specification and verification of systems, specially in LTL of 𝑀 , that is, ℒ(𝐴𝜙 ) = { 𝜋 ∈ 𝒫(AP )𝜔 | 𝜋 |= 𝜙 }, and model checking [11]. Büchi automata have also been used in ℒ(𝐴𝑀 ) = Traces(𝑀 ). planning to synthesize plans when goals are in LTL [26, 30]. The proposition above states that every LTL formula 𝜙 can be expressed as a Büchi automaton 𝐴𝜙 , in the sense that Definition 6 (Büchi Automata). A Büchi automaton is a 𝐴𝜙 accepts exactly all the traces satisfying 𝜙. This result tuple 𝐴 = (𝑄, Σ, ∆, 𝑄0 , 𝑅) consisting of a finite set of states allows to decide if a formula 𝜙 is satisfiable, by deciding 𝑄; a finite, nonempty alphabet Σ (whose elements are called emptiness of ℒ(𝐴𝜙 ). Analogously, a Büchi automaton 𝐴𝑀 letters); a transition relation ∆ ⊆ 𝑄 × Σ × 𝑄; a set of initial can be used to capture precisely all the traces from a given states 𝑄0 ⊆ 𝑄; and a set of recurrence states 𝑅 ⊆ 𝑄. Kripke structure 𝑀 , as Proposition 8 states. These two observations make it possible to decide LTL model-checking, We show a concrete Büchi automaton in Example 7. by deciding the inclusion ℒ(𝐴𝑀 ) ⊆ ℒ(𝐴𝜙 ). In Section 5, A Büchi automaton accepts an infinite word over a fi- we will exploit Proposition 8 to devise mechanisms that nite alphabet Σ, if the automaton visits a recurrence state support the computation of belief change operators in LTL. infinitely often while reading the word. Formally, an in- finite word is a sequence 𝑎0 𝑎1 . . . with 𝑎𝑖 ∈ Σ for all 𝑖. For a finite word 𝜌 = 𝑎0 . . . 𝑎𝑛 , with 𝑛 ≥ 0, let 𝜌𝜔 denote 3. AGM Contraction the infinite word corresponding to the infinite repetition of 𝜌. The set of all infinite words is denoted by Σ𝜔 . An In the AGM paradigm, the epistemic state of an agent is infinite word 𝑎0 𝑎1 𝑎2 . . . ∈ Σ𝜔 is accepted by a Büchi au- represented as a theory. A contraction function for a theory . 𝒦 is a function − : Fm → 𝒫(Fm) that given an unwanted tomaton 𝐴 = (𝑄, Σ, ∆, 𝑄0 , 𝑅) if there exists a sequence 𝑞0 , 𝑞1 , 𝑞2 , . . . of states 𝑞𝑖 ∈ 𝑄 such that 𝑞0 ∈ 𝑄0 is an ini- piece of information 𝜙 outputs a subset of 𝒦 which does not tial state, for all 𝑖 we have that (𝑞𝑖 , 𝑎𝑖 , 𝑞𝑖+1 ) ∈ ∆ and there entail 𝜙. Contraction functions are subject to the following are infinitely many 𝑖 ∈ N with 𝑞𝑖 ∈ 𝑅. The set ℒ(𝐴) of all rationality postulates [2]: accepted words is the language of 𝐴. . . (K− 1 ) 𝒦 − 𝜙 = Cn(𝒦 − 𝜙) (closure) In this work, unless otherwise noted, we always consider . (K− 2) 𝒦− 𝜙 ⊆ 𝒦 (inclusion) Büchi automata over the alphabet Σ = 𝒫(AP ), where . letters are sets of atomic propositions and infinite words are 3 ) If 𝜙 ̸∈ 𝒦, then 𝒦 − 𝜙 = 𝒦 (K− (vacuity) (K− ) If 𝜙 ∈ ̸ Cn(∅), then 𝜙 ∈ ̸ 𝒦 − . 𝜙 (success) traces. The following example presents such an automaton. 4 . (K− 5 ) 𝒦 ⊆ (𝒦 − 𝜙) + 𝜙 (recovery) Example 7. Figure 2 illustrates (on the left) a Büchi automa- . . (K6 ) If 𝜙 ≡ 𝜓, then 𝒦 − 𝜙 = 𝒦 − 𝜓 (extensionality) − ton 𝐴𝒦 over the alphabet Σ = {∅, {𝑝}}. States are depicted (K− . . . 7 ) (𝒦 − 𝜙) ∩ (𝒦 − 𝜓) ⊆ 𝒦 − (𝜙 ∧ 𝜓) as circles and each transition (𝑞, 𝑎, 𝑞 ′ ) is depicted as an arrow . . . 8 ) If 𝜙 ̸∈ 𝒦 − (𝜙 ∧ 𝜓) then 𝒦 − (𝜙 ∧ 𝜓) ⊆ 𝒦 − 𝜙 (K− from 𝑞 to 𝑞 ′ labelled with 𝑎. The initial state is 𝑞0 , and the recurrence states are marked as double circles, i. e., 𝑞1 and 𝑞2 . For a detailed discussion on the rationale of these postu- The right-hand side of Figure 2 shows some of the infinite lates, see [1, 2, 3]. The postulates (K− 1 ) to (K6 ) are called − words accepted by the Büchi automaton 𝐴𝒦 . Consider, for the basic rationality postulates, while (K− 7 ) and (K−8 ) are instance, the sequence known as supplementary postulates. A contraction func- tion that satisfies the basic rationality postulates is called ∅ ∅ ∅ {𝑝} 𝑞0 → 𝑞0 → 𝑞0 → 𝑞1 → 𝑞2 → 𝑞1 → 𝑞2 . . . , ∅ {𝑝} a rational contraction function. If a contraction function satisfies all the eight rationality postulates, we say that it is resemble the cognitive states of human minds, and Hans- fully rational. son argues that as “finite beings”, humans cannot sustain There are many different constructions for (fully) ratio- epistemic states that do not have a finite representation. Fur- nal AGM contraction such as Partial Meet [1], Epistemic ther, finite representation is crucial from a computational Entrenchment [2], and Kernel Contraction [6]. All these perspective, to represent epistemic states in a computer. functions are characterized by the AGM postulates of con- Different strategies of finite representation have been traction. For an overview, see [31, 3]. These contraction used such as (i) finite bases [35, 36, 37], and (ii) finite sets of functions, however, are rational only in very specific logics, models [38, 39]. In the former strategy, each finite set 𝑋 of precisely in the presence of the AGM assumptions [8] which formulae, called a finite base, represents the theory Cn(𝑋). includes requiring the logic to be Boolean and compact. See In the latter strategy, models are used to represent an epis- [8] for details about the AGM assumptions. temic state. Precisely, each finite set 𝑋 of models represents To embrace more expressive logics, Ribeiro et al. [18] have the theory of all formulae satisfied by all models in 𝑋, that proposed a new class of (fully) rational contraction functions is, the theory {𝜙 ∈ Fm L | 𝑀 |= 𝜙, for all 𝑀 ∈ 𝑋}. which only assume the underlying logic to be Tarskian and The expressiveness of finite bases and finite sets of models Boolean: the Exhaustive Contraction Functions (for basic are, in general (depending on the logic), incomparable, that rationality) and the Blade Contraction Functions (for full is, some theories expressible in one method cannot be ex- rationality). We briefly review Exhaustive Contraction Func- pressed in the other method and vice versa. For instance, tions. We do not delve into the Blade Contraction Functions, the information that “John swims every two days” cannot as our results for full rationality do not use such functions, be expressed via a finite base in LTL [40], although it can but rather use the supplementary postulates directly. be expressed via a single Kripke structure (shown in Fig. 1, where 𝑝 stands for “John swims”). On the other hand, “Anna Definition 9 (Choice Functions). A choice function is a will swim eventually” is expressible as a single LTL formula function 𝛿 : Fm → 𝒫(CCT) maps each formula 𝜙 to a set (F 𝑠, where 𝑠 stands for “Anna swims”), but it cannot be of complete consistent theories satisfying the following: expressed via a finite set of models. Given the incomparable expressiveness of these two well- (CF1) 𝛿(𝜙) ̸= ∅; established strategies of finite representations, it is not clear (CF2) if 𝜙 ̸∈ Cn(∅), then 𝛿(𝜙) ⊆ 𝜔(𝜙); and whether in general, and specifically in non-finitary logics, there exists a method capable of finitely representing all (CF3) for all 𝜙, 𝜓 ∈ Fm, if 𝜙 ≡ 𝜓 then 𝛿(𝜙) = 𝛿(𝜓). theories, therefore capturing the whole expressiveness of the logic. Towards answering this question, we provide a A choice function chooses at least one complete consis- broad definition to conceptualise finite representation. tent theory, for each formula 𝜙 to be contracted (CF1). As A finite representation for a theory can been seen as a long as 𝜙 is not a tautology, the CCTs chosen must not con- finite word, i.e., a code, from a fixed finite alphabet ΣC . For tain the formula 𝜙 (CF2), since the goal is to relinquish 𝜙. example, the codes 𝑐1 := {a, b} and 𝑐2 := {a, a→b} The last condition (CF3) imposes that a choice function is are finite words in the language of set theory, and both syntax-insensitive. represent the theory Cn({𝑎 ∧ 𝑏}). The set of all codes, i.e., Definition 10 (Exhaustive Contraction Functions). Let 𝛿 of all finite words over ΣC , is denoted by Σ*C . In this sense, be a choice function. The Exhaustive Contraction Function a method of finite representation is a mapping 𝑓 from codes (ECF) on a theory 𝒦 induced . by 𝛿 is the function −𝛿 such in Σ*C to theories. The pair (ΣC , 𝑓 ) is called an encoding. . ⋂︀ that 𝒦 −𝛿 𝜙 = 𝒦 ∩ 𝛿(𝜙), if 𝜙 ∈ / Cn(∅) and 𝜙 ∈ 𝒦; . Definition 12 (Encoding). An encoding (ΣC , 𝑓 ) comprises otherwise, 𝒦 −𝛿 𝜙 = 𝒦. a finite alphabet ΣC and a partial function 𝑓 : Σ*C ⇀ ThL . Whenever the formula 𝜙 to be contracted is not a tautol- Given an encoding (ΣC , 𝑓 ), a word 𝑤 ∈ Σ*C represents a ogy and is in the theory 𝒦, an ECF modifies the current the- theory 𝒦, if 𝑓 (𝑤) is defined and 𝑓 (𝑤) = 𝒦. Observe that a ory by selecting some CCTs and intersecting them with 𝒦. theory might have more than one code, whereas for others On the other hand, if 𝜙 is either a tautology or is not in there might not exist a code. For instance, in the example the theory 𝒦, then all beliefs are preserved. The ECFs are above for finite bases, the codes 𝑐1 and 𝑐2 represent the similar in spirit to the standard partial meet functions [1]. same theory. On the other hand, recall that the LTL theory The main difference is that partial meet relies on the internal corresponding to “John swims every two days” cannot be structure of the current theory by selecting and intersect- expressed in the finite base encoding. Furthermore, the func- ing remainders (maximal non-entailing subsets), whilst ECF tion 𝑓 is partial, because not all codes in Σ*C are meaningful. chooses external structures (CCTs). In the latter, CCTs are For instance, for the finite base encoding, the code {{}} used, because, in the absence of compactness, remainders cannot be interpreted as a finite base. do not exist in general [12, 18, 32]. We are interested in logics which are AGM compliant, . Theorem 11. [18] A contraction function − is rational iff that is, logics in which rational contraction functions exist. it is an ECF. Unfortunately, it is still an open problem how to construct AGM contraction functions in all such logics. The most gen- eral constructive apparatus up to date, as discussed in Sec- 4. Limits of Finite Representation tion 3, are the Exhaustive Contraction functions proposed by Ribeiro et al. (2018) which assume only few conditions on In the AGM paradigm, the epistemic states of an agent are the logic. Additionally, we focus on non-finitary logics, as represented as theories which are in general infinite. How- the finitary case is trivial. We call such logics compendious. ever, according to Hansson [33, 34], the epistemic states of rational agents should have a finite representation. This is Definition 13 (Compendious Logics). A logic L is compen- motivated from the perspective that epistemic states should dious if L is Tarskian, Boolean, non-finitary and satisfies: Büchi automaton 𝐴𝒦 : Supported Formulae: (Discerning) ⋂︀ ⋂︀ all sets 𝑋, 𝑌 ⊆ CCTL , we have that For 𝑋 = 𝑌 implies 𝑋 = 𝑌 . ∅,{𝑝} F 𝑝 ∈ 𝒮(𝐴𝒦 ) {𝑝} G F 𝑝 ∈ 𝒮(𝐴𝒦 ) Compendiousness amounts to expressivity in multiple di- 𝑞0 ∅,{𝑝} 𝑞1 𝑞2 2 F (𝑝 → X 𝑝 ∨ X 𝑝) ∈ 𝒮(𝐴𝒦 ) mensions. Compendious logics can express infinitely many G 𝑝, ¬(G 𝑝) ∈ / 𝒮(𝐴𝒦 ) ∅, {𝑝} distinct sentences (non-finitary), distinguish between a sen- tence being true or false (classical negation), and express Figure 3: A Büchi automaton, along with some examples of uncertainty of two or more sentences (disjunction). The supported (and not supported) LTL formulae. property (Discerning) is related the possible worlds seman- tics. 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 support reasoning. Most fundamentally, an agent should epistemic state is interpreted as the exact set of all possi- be able to decide whether it believes a given formula 𝜙, i.e., ble worlds in which all the agent’s beliefs are true. If the whether 𝜙 is entailed by the theory representing the agent’s truth value of a formula 𝜙 is unknown, the agent considers epistemic state. This question might be decidable for one some possible worlds where 𝜙 is true, as well as possible (perhaps less expressive) encoding, but undecidable for a worlds where 𝜙 is false. Hence, more possible worlds indi- different (more expressive) encoding. We call this question cate strictly less information. Equivalently, different sets of the entailment problem on an encoding (ΣC , 𝑓 ): possible worlds represent different epistemic states. This is Input: (𝑤, 𝜙) ∈ Σ*C × Fm L , such that 𝑓 (𝑤) is defined exactly what (Discerning) conceptualises. Output: true if 𝜙 ∈ 𝑓 (𝑤), otherwise false Example 14 (Discerning). Yara and Yasmin encounter a large flightless bird. Yara knows that such birds exist in Africa This problem is a generalisation of several decision prob- and South America. Hence, Yara considers two possible worlds: lems that support reasoning. For example, on the finite base the bird is from Africa (it is an ostrich), or the bird is from encoding, it corresponds to the usual entailment problem South America (it is a rhea). Yasmin, who lived in Australia, between formulae. Entailment on the encoding based on believes the bird is an emu (from Australia), a rhea or an os- finite sets of models corresponds to the model checking trich. Since Yara and Yasmin consider different sets of possible problem. For other encodings, as we will see, it can be more worlds, their epistemic states differ. Yara believes in the dis- general than either of these problems. junction ostrich ∨rhea, Yasmin does not. She believes only in We investigate a suitable encoding for epistemic states the disjunction ostrich ∨ rhea ∨ emu. As per (Discerning), over LTL, a commonly used compendious logic in model Yara and Yasmin present different epistemic states, due to the checking and planning. In both these domains, the primary difference in the considered possible worlds. approach to reason about LTL is based on Büchi automata. The class of compendious logics is broad and includes Thus, from a reasoning standpoint, Büchi automata are several widely used logics. predestined to be the basis for an encoding of epistemic states over LTL. We give the following definition for the set Theorem 15. The logics LTL, CTL, CTL*, 𝜇-calculus and of LTL formulae represented by a Büchi automaton: monadic second-order logic (MSO) are compendious. Definition 18 (Support). The support of a Büchi automaton It turns out that there is no method of finite representation 𝐴 is the set 𝒮(𝐴) := { 𝜙 ∈ Fm LTL | ∀𝜋 ∈ ℒ(𝐴) . 𝜋 |= 𝜙 }. capable of capturing all theories in a compendious logic. If 𝜙 ∈ 𝒮(𝐴), we say that 𝐴 supports 𝜙. Theorem 16. No encoding can represent every theory of a Example 19. Figure 3 shows a Büchi automaton (on the compendious logic. left), along with three supported formulae (on the right). All Proof Sketch. We show that, since compendious logics are accepted traces satisfy these formulae. The formula G 𝑝 is not Tarskian, Boolean and non-finitary, there exist infinitely supported. While some accepted traces, such as {𝑝}𝜔 , satisfy many CCTs. From (Discerning), it follows that there ex- this formula, others, such as ∅ {𝑝}𝜔 do not. Consequently, the ist uncountably many theories in the logic. However, an negation ¬(G 𝑝) is not supported either. encoding can represent only countably many theories. It remains to show that the support of a Büchi automaton is a theory. Perhaps surprisingly, the support of an arbi- As not every theory cann be finitely represented, only trary language of infinite traces (not represented as a Büchi some subsets of theories can be used to express the epistemic automaton) does not necessarily form a theory. The discon- states of an agent. We call a subset E of theories an excerpt nect arises from the fact that the semantics of LTL is defined of the logic. Each encoding induces an excerpt. over finite Kripke structures, and arbitrary languages of Definition 17. The excerpt induced by an encoding (ΣC , 𝑓 ) infinite traces can represent more fine-grained nuances of is the set E := img(𝑓 ). An excerpt induced by some encoding behaviours. Consider the language 𝐿prime = {𝑎0 𝑎1 𝑎2 . . .}, is called finitely representable. where 𝑎𝑖 = {𝑝} if 𝑖 is a prime number and 𝑎𝑖 = ∅ other- wise. The support of 𝐿prime prescribes that 𝑝 holds exactly in prime-numbered steps. Since no Kripke structure satisfies 5. The Büchi Encoding of LTL this requirement, the support of 𝐿prime is inconsistent, yet 𝐿prime does not support ⊥. The encoding in which epistemic states are expressed is of An intriguing property of Büchi automata however is fundamental importance. On the one hand, the encoding that their support is fully determined by those accepted must be expressive enough to capture a non-trivial space traces 𝜋 that have the property of being ultimately periodic, of epistemic states. On the other hand, the encoding must that is, 𝜋 = 𝜌 𝜎 𝜔 for some finite sequences 𝜌, 𝜎. Recall from Section 2.2 that the superscript 𝜔 denotes infinite rep- By contrast, the following two sections discuss funda- etition of the subsequence 𝜎. Ultimately periodic traces mental limitations to effective constructions for rational are tightly connected to CCTs: each CCT is satisfied by contractions. Nevertheless, we show in Section 8 how the exactly one ultimately periodic trace. Let UP denote the Büchi encoding admits similar automata-based construc- set of all ultimately periodic traces. The correspondence tions for a large subclass of contraction functions. between CCTs and ultimately periodic traces is formal- ized by the function Th UP : UP → CCTLTL such that Th UP (𝜋) = {𝜙 ∈ Fm LTL | 𝜋 |= 𝜙}. 6. AGM Accommodation Lemma 20. The function Th UP is a bijection. Assume that the space of epistemic states that an agent can entertain is determined by an excerpt E. In this section, We combine Lemma 20 with two classical observa- we investigate which properties make an excerpt suitable tions [11]: (i) every consistent LTL formula is satisfied by at from the AGM vantage point. Clearly, not every excerpt is least one ultimately periodic trace; and (ii) every Büchi au- suitable for representing the space of epistemic states. For tomaton with nonempty language accepts some ultimately example, if a non-tautological formula 𝜙 appears in each periodic trace. We arrive at the following characterization: theory of E, then 𝜙 cannot be contracted. The chosen ex- Lemma 21. The support of a Büchi automaton 𝐴 satisfies cerpt 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 ⋂︁ 𝒮(𝐴) = { Th UP (𝜋) | 𝜋 ∈ ℒ(𝐴) ∩ UP } . piece of information and changes its epistemic state into Theorem 22. The support of a Büchi automaton is a theory. a new one, then this new epistemic state must be express- ible in the underlying excerpt. A straightforward option Thus, Büchi automata indeed define an encoding. Ev- would be to require some sort of closure under AGM ratio- ery Büchi automaton 𝐴, being a finite structure, can be nality, that is, all possible rational contractions involving described in a finite code word 𝑤𝐴 , which the encoding information in the excerpt should be expressed yet within maps to the theory 𝒮(𝐴). We call this encoding the Büchi the excerpt. Such excerpts are closed under rational con- encoding, denoted (ΣBüchi , 𝑓Büchi ), and the induced excerpt traction resp. under fully rational contraction. We say that a the Büchi excerpt EBüchi . In terms of expressiveness, the . . contraction − remains in E if img(−) ⊆ E. Büchi excerpt strictly subsumes the classical approaches: Definition 25 (Closedness). An excerpt E of a logic L is Theorem 23. Let Ebase and Emodels denote respectively the closed under (fully) rational contraction iff for all theories excerpts of finite bases and finite sets of models2 . It holds that 𝒦 ∈ E, every (fully) rational contraction operation on 𝒦 Ebase ∪ Emodels ⊊ EBüchi . remains in E. Proof Sketch. The expressiveness of the Büchi excerpt fol- Closedness maximises the expressiveness of the excerpt lows from Proposition 8. Figure 3 shows an automaton w.r.t. AGM rationality: in each epistemic state of the excerpt, whose support can be expressed neither by a finite base nor every possible (fully) AGM rational contraction outcome is a finite sets of models. at disposal. However, although closedness might seem like a reasonable condition, it turns out to be very demanding. In terms of reasoning, the Büchi encoding benefits from For example, as we are dealing with Boolean logics, which the decidability properties of Büchi automata. Many deci- are closed under classical negation, an agent should be able sion problems, most importantly the entailment problem on to either accept or reject some pieces of information. The the Büchi encoding, can be reduced to the decidable problem excerpt should be broad enough such that there exists some of inclusion between Büchi automata. piece of information 𝜙, where both 𝜙 and ¬𝜙 occur in some, Theorem 24. The entailment problem on the Büchi encoding possibly different, epistemic states of the excerpt. We call is decidable. such excerpts open-minded. Even under such an innocuous condition, an agent cannot express its epistemic states in an Proof. Given a word 𝑤 ∈ Σ*Büchi that encodes a Büchi au- excerpt that is closed under rational contraction: closedness tomaton 𝐴𝑤 , and an LTL formula 𝜙, one can decide whether rules out finite representability. 𝜙 ∈ 𝑓Büchi (𝑤) = 𝒮(𝐴𝑤 ) by deciding the Büchi automata inclusion ℒ(𝐴𝑤 ) ⊆ ℒ(𝐴𝜙 ). Theorem 26 (Impossibility of Closedness). If E is an open- minded, finitely representable excerpt of a compendious logic, Beyond ensuring the decidability of key problems, an en- then E is not closed under rational contraction. coding’s suitability for reasoning also involves the question whether modifications of epistemic states can be realized Proof Sketch. From open-mindedness, it follows that there by computations on code words. In particular in the con- exists a formula 𝜙 in a theory 𝒦 of the excerpt, such that text of the AGM paradigm, it is interesting to see if belief 𝜔(𝜙) is infinite. Then there are already uncountably many change operations can be performed in such a manner. The ways to contract 𝜙. However, the finitely representable Büchi encoding also shines in this respect, since we can excerpt contains only countably many theories. employ automata operations to this end. As a first exam- The negative result above concerns excerpts that are ple, consider the expansion of a theory 𝒦 with a formula 𝜙. closed under rational contraction. As full rationality is This operation corresponds to an intersection operation on strictly more demanding than rationality, one could hope Büchi automata, as the support of a Büchi automaton satis- to reach closedness by restricting to excerpts closed under fies 𝒮(𝐴) + 𝜙 = 𝒮(𝐴 ⊓ 𝐴𝜙 ). The intersection automaton fully rational contraction. Unfortunately, rationally closed 𝐴 ⊓ 𝐴𝜙 can be computed through a product construction. excerpts and fully rationally closed excerpts coincide. 2 These excerpts were described in the prologue of Section 4. Proposition 27. An excerpt is closed under fully rational states could be expressed in a finitary logic. As the com- contraction iff it is closed under rational contraction. putability in the finitary case is trivial, we focus on the more expressive case. Instead of insisting on maximising the expressiveness of the excerpts, we impose a weaker condition and require the Definition 31 (Non-Finitary). A theory 𝒦 is non-finitary excerpt only to admit at least one rational outcome for each if it contains infinitely many logical equivalence classes of possible contraction. formulae. Definition 28 (Accommodation). An excerpt E accommo- Note that being non-finitary is a very general condition. dates (fully) rational contraction iff for each 𝒦 ∈ E there Even theories with a finite base can be non-finitary. For exists a (fully) rational contraction on 𝒦 that remains in E. instance, the LTL theory Cn(G 𝑝) contains the infinitely many non-equivalent formulae {𝑝, X 𝑝, X2 𝑝, X3 𝑝, . . .}. Accommodation guarantees that an agent can modify its In the remainder of this section, we establish a strong beliefs rationally, in all possible epistemic states covered by link between non-finitary theories and uncomputable con- the excerpt. There is a clear connection between accom- traction functions. To this end, we introduce the notion of modation and AGM compliance. While AGM compliance cleavings. concerns existence of rational contraction operations in ev- ery theory of a logic, accommodation guarantees that the Definition 32 (Cleaving). A cleaving is an infinite set of information in each theory within the excerpt can be ratio- formulae 𝒞 such that for all two distinct 𝜙, 𝜓 ∈ 𝒞 we have: nally contracted and that its outcome can yet be expressed within the excerpt. Analogous to closedness, rational ac- (CL1) 𝜙 and 𝜓 are not equivalent (𝜙 ̸≡ 𝜓); and commodation and fully rational accommodation coincide. (CL2) the disjunction 𝜙 ∨ 𝜓 is a tautology. Proposition 29. An excerpt E accommodates rational con- From an algebraic perspective, the formulae in a cleaving traction iff E accommodates fully rational contraction. behave like a kind of weak complement: we require that the disjunction 𝜙 ∨ 𝜓 is a tautology, whereas we do not require 7. Uncomputability of Contraction the conjunction 𝜙 ∧ 𝜓 to be inconsistent (as would be the case for the conjunction 𝜙 ∧ ¬𝜙). Accommodation is the weakest condition we can impose upon an excerpt to guarantee the existence of AGM rational Example 33. Consider the logic of elementary arithmetic contractions. Yet, the existence of contractions does not im- over natural numbers. The formulae 𝑥 ̸= 0, 𝑥 ̸= 1, 𝑥 ̸= 2, ply that an agent can effectively contract information. Thus etc. form a cleaving: they are pairwise non-equivalent, and we investigate the question of computability of contraction every disjunction (𝑥 ̸= 𝑖) ∨ (𝑥 ̸= 𝑗) is a tautology (where functions. For this endeavor, the focus on contraction func- 𝑖, 𝑗 are two different constants). tions that remain in the excerpt is crucial: both input and Example 34. Let twice(𝑝) :≡ F (𝑝 ∧ X F 𝑝) be the LTL output of a computation must be finitely representable. We formula denoting that proposition 𝑝 holds at least twice, and thus fix a finitely representable excerpt E that accommo- for 𝑖 ∈ N, let 𝜓𝑖 :≡ (X𝑖 𝑝) → twice(𝑝) be the formula dates contraction. As an agent has to reason about its beliefs, stating that if 𝑝 holds in time step 𝑖, it must hold at least it should be able to decide whether two formulae are logi- one additional time (i.e., at least twice overall). For 𝑖 ̸= 𝑗, cally equivalent. Hence, we assume that, in the underlying the formulae 𝜓𝑖 and 𝜓𝑗 are non-equivalent. Further, the logic, logical equivalence is decidable. disjunction 𝜓𝑖 ∨𝜓𝑗 simplifies to (X𝑖 𝑝)∧(X𝑗 𝑝) → twice(𝑝). Definition 30 (AGM Computability). Let 𝒦 be a theory in The latter formula is a tautology: if 𝑝 holds in time steps . E, and let − be a contraction function on 𝒦 that remains in 𝑖 and 𝑗, it holds at least twice. Hence, the set of formulae . E. We say that − is computable if there exists an encoding {𝜓0 , 𝜓1 , . . .} is a cleaving. (ΣC , 𝑓 ) that induces E, such that the following problem is Lemma 35. Every non-finitary theory contains a cleaving. computed by a Turing machine: Given a contraction that remains in an excerpt, cleavings Input: A formula 𝜙 ∈ Fm L . provide a way of generating many different contractions . that remain within the excerpt. This works by ranking the Output: A word 𝑤 ∈ Σ*C such that 𝑓 (𝑤) = 𝒦 − 𝜙. formulae in the cleaving such that each rank has exactly In the classical setting of finitary logics, computability of one formula. We reduce the contraction of a formula 𝜙 to AGM contraction is trivial, as there are only finitely many contracting 𝜙 ∨ 𝜓, where 𝜓 is the lowest ranked formula in formulae (up to equivalence), and only a finite number of the cleaving such that 𝜙 ∨ 𝜓 is non-tautological. Each new theories. By contrast, compendious logics have infinitely contraction depends on the original choice function and the many formulae (up to equivalence) and consequently in- ranking. finitely many theories. Definition 36 (Composition). Let 𝛿 be a choice function In the following, unless otherwise stated, we only con- on a theory 𝒦, 𝒞 ⊆ 𝒦 be a cleaving, and 𝜋 : N → 𝒞 be a sider compendious logics. In such logics, we distinguish permutation of 𝒞. The composition of 𝛿 and 𝜋 is the function two kinds of theories: those that contain infinitely many 𝛿𝜋 : Fm → 𝒫(CCT) such that formulae (up to equivalence), and those that contain only finitely many formulae (up to equivalence). An excerpt (︀ )︀ 𝛿𝜋 (𝜙) := 𝛿 𝜙 ∨ min𝜋 (𝜙) that constrains an agent’s epistemic states to the latter case essentially disposes of the expressive power of the compen- where min𝜋 (𝜙) = 𝜋(𝑖), for the minimal 𝑖 ∈ N such that dious logic, as in each epistemic state only finitely many 𝜙 ∨ 𝜋(𝑖) ̸≡ ⊤, or min𝜋 (𝜙) = ⊥ if no such 𝑖 exists. sentences can be distinguished. Therefore, such epistemic 𝐴¬G F 𝑝 : 𝐴𝒦 ⊔ 𝛾(G F 𝑝): Example 37. Consider the cleaving {𝜓0 , 𝜓1 , . . .} of Exam- ∅, {𝑝} ∅ ∅, {𝑝} ple 34, and let 𝜋 be the permutation with 𝜋(𝑖) = 𝜓𝑖 for all {𝑝} 𝑖 ∈ N. The formula 𝑝 ∨ 𝜓0 is a tautology. Thus, we have ∅ ∅, {𝑝} 𝑝1 𝑝2 𝑞0 𝑞1 𝑞2 min𝜋 (𝑝) = 𝜋(1) = 𝜓1 and the choice function chooses 𝛿𝜋 (𝑝) = 𝛿(𝑝 ∨ 𝜓1 ). If we however consider a permuta- ∅, {𝑝} 𝛾(G F 𝑝): tion 𝜋 ′ with 𝜋 ′ (0) = 𝜓2 and 𝜋 ′ (2) = 𝜓0 , then we have {𝑝} ∅ min𝜋′ (𝑝) = 𝜋 ′ (0) = 𝜓2 and 𝛿𝜋′ (𝑝) = 𝛿(𝑝 ∨ 𝜓2 ). ∅, {𝑝} ∅ 𝑧1 𝑧2 𝑧3 If we consider the formula F G ¬𝑝 stating that 𝑝 only holds {𝑝} ∅ 𝑧1 𝑧2 𝑧3 finitely 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 Figure 4: BCF contraction of G F 𝑝 from 𝒮(𝐴𝒦 ) (Example 43). twice. Hence, we have, (︀ for both permutations, )︀ 𝛿𝜋 (F G ¬𝑝) = 𝛿𝜋′ (F G ¬𝑝) = 𝛿 (F G ¬𝑝) ∨ ⊥ = 𝛿(F G ¬𝑝). designed such that the intersection of 𝒦 with the selected The composition of a choice function 𝛿 with a permuta- CCTs corresponds to the support of a Büchi automaton. As tion of a cleaving preserves rationality. CCTs and ultimately periodic traces are interchangeable Lemma 38. The composition 𝛿𝜋 of a choice function 𝛿 and (Lemma 20), and the support of a Büchi automaton is deter- a permutation 𝜋 : N → 𝒞 of a cleaving 𝒞 ⊆ 𝒦 is a choice mined by the CCTs corresponding to its accepted ultimately function. periodic traces (Lemma 21), a solution is to design a selec- tion mechanism, analogous to choice functions, that picks a A composition generates a new choice function which in single Büchi automaton instead of an (infinite) set of CCTs. turn induces a rational contraction function that remains within the excerpt. Yet, the induced contraction function is Definition 40 (Büchi Choice Functions). A Büchi choice not necessarily computable. function 𝛾 maps each LTL formula to a single Büchi automa- ton, such that for all LTL formulae 𝜙 and 𝜓, Theorem 39. Let E accommodate rational contraction, and let 𝒦 ∈ E. The following statements are equivalent: (BF1) the language accepted by 𝛾(𝜙) is non-empty; 1. The theory 𝒦 is non-finitary. (BF2) 𝛾(𝜙) supports ¬𝜙, if 𝜙 is not a tautology; and 2. There exists an uncomputable rational contraction (BF3) 𝛾(𝜙) and 𝛾(𝜓) accept the same language, if 𝜙 ≡ 𝜓. function on 𝒦 that remains in E. 3. There exists an uncomputable fully rational contrac- Conditions (BF1) - (BF3) correspond to the respective tion function on 𝒦 that remains in E. conditions (CF1) - (CF3) in the definition of choice functions. Each Büchi choice function induces a contraction function. Proof Sketch. Let 𝒦 be non-finitary, and 𝛿 the choice func- tion of a (fully) rational contraction for 𝒦 that remains in E. Definition 41 (Büchi Contraction Functions). Let 𝒦 be a Each permutation 𝜋 of a cleaving 𝒞 ⊆ 𝒦 induces a distinct theory in the Büchi excerpt and let 𝛾 be a Büchi choice function. (fully) rational contraction (with choice function 𝛿𝜋 ) that The Büchi Contraction Function (BCF) on 𝒦 induced by 𝛾 is remains in E. At most countably many of these uncountably the function many (fully) rational contractions can be computable. {︃ If 𝒦 is finitary, every contraction function is computable, . 𝒦 ∩ 𝒮(𝛾(𝜙)) if 𝜙 ∈ / Cn(∅) and 𝜙 ∈ 𝒦 𝒦 −𝛾 𝜙 = as it only has to consider finitely many formulae. 𝒦 otherwise Theorem 39 makes evident that uncomputability of AGM All such contractions remain in the Büchi excerpt. Indeed, contraction is inevitable. In fact, there are uncountably one can observe that if 𝒦 = 𝒮(𝐴) for a Büchi automaton many uncomputable contraction functions. The only way 𝐴, it holds that 𝒦 ∩ 𝒮(𝛾(𝜙)) = 𝒮(𝐴 ⊔ 𝛾(𝜙)). Recall from to avoid this uncomputability would be to restrain the ex- Section 2 that ⊔ denotes the union of Büchi automata. The pressiveness of the excerpt to the most trivial case: only class of all rational contraction functions that remain in the finitary theories. Büchi excerpt corresponds exactly to the class of all BCFs. Theorem 42. A contraction function − on a theory . 8. Effective Contraction in the Büchi 𝒦 ∈ EBüchi is rational and remains within the Büchi excerpt . if and only if − is a BCF. Excerpt Despite the strong negative result of Section 7, computability Example 43. Let 𝒦 = 𝒮(𝐴𝒦 ), for the Büchi automaton can still be harnessed in very particular excerpts: excerpts 𝐴𝒦 shown in Fig. 3. To contract the formula G F 𝑝, a Büchi E in which for every theory, there exists at least one com- choice function 𝛾 may select the Büchi automaton 𝛾(G F 𝑝) putable (fully) rational contraction function that remains in shown in Fig. 4. This automaton supports ¬G F 𝑝; the au- E. We say that such an excerpt E effectively accommodates tomaton 𝐴¬G F 𝑝 is shown for reference. In fact, 𝛾(G F 𝑝) (fully) rational contraction. If belief contraction is to be com- accepts precisely the traces satisfying 𝑝 ∧ ¬G F 𝑝. The re- puted for compendious logics, it is paramount to identify sult of the contraction is the theory 𝒮(𝐴𝒦 ) ∩ 𝒮(𝛾(G F 𝑝)), such excerpts as well as classes of computable contraction which corresponds to the theory 𝒮(𝐴𝒦 ⊔ 𝛾(G F 𝑝)), whose functions. In this section, we show that the Büchi excerpt of supporting automaton is also shown in Fig. 4. The union ⊔ is LTL effectively accommodates (fully) rational contraction. obtained by simply taking the union of states and transitions. For a contraction on a theory 𝒦 ∈ EBüchi to remain in This automaton does not support G F 𝑝, and therefore the the Büchi excerpt, the underlying choice function must be contraction is successful. As BCFs capture all rational contractions within the ex- can be properly defined. Such logics are called relevance- cerpt, it follows from Theorem 39 that not all BCFs are compliant. As relevance is an weakened version of recovery, computable. Note from Definition 41 that to achieve com- the uncomputability results in this work translate to var- putability, it suffices to be able to: (i) decide if 𝜙 is a tau- ious relevance-compliant logics. However, it is unclear if tology, (ii) decide if 𝜙 ∈ 𝒦, (iii) compute the underlying all such logics are affected by uncomputability. We aim to Büchi choice function 𝛾, and (iv) compute the intersection investigate this issue in such logics. of 𝒦 with the support of 𝛾(𝜙). We already know that con- Even if we have to coexist with uncomputability, we can ditions (i) and (ii) are satisfied (Theorem 24). For condi- still identify classes of operators which are guaranteed to be tion (iv), recall that the intersection of the support of two computable. To this end, we have introduced a novel class automata is equivalent to the support of their union. As 𝛾 of contraction functions for LTL using Büchi automata, and produces a Büchi automaton, and union of Büchi automata identified the conditions needed for computability. This is is computable, condition (iv) is also satisfied. Therefore, an initial step towards the application of belief change in condition (iii) is the only one remaining. It turns out that other areas, such as methods for automatically repairing (iii) is a necessary and sufficient condition to characterize all systems [45]. The methods devised here for LTL form a computable contraction functions within the Büchi excerpt. foundation for the development of analogous strategies for . other expressive logics, such as CTL, 𝜇-calculus and many Theorem 44. Let − be a rational contraction function on Description Logics. For example, in these logics, similarly to . a theory 𝒦 ∈ EBüchi , such that − remains in the Büchi ex- . . . LTL, decision problems such as satisfiability and entailment cerpt. The operation − is computable iff − = −𝛾 for some have been solved using various kinds of automata, such as computable Büchi choice function 𝛾 . tree automata [46, 47]. Note that there do indeed exist computable choice func- tions. As an example, the full meet contraction [1, 3] is References computable. The corresponding Büchi choice function 𝛾fm is given by 𝛾fm (𝜙) = 𝐴¬𝜙 if 𝜙 is non-tautological, and [1] C. E. Alchourrón, P. Gärdenfors, D. Makinson, On the 𝛾fm (𝜙) = 𝐴⊤ otherwise. This function is computable: the logic of theory change: Partial meet contraction and automata 𝐴¬𝜙 and 𝐴⊤ can be effectively constructed, and it revision functions, J. Symb. Log. 50 (1985) 510–530. is decidable whether the given LTL formula 𝜙 is a tautology. doi:10.2307/2274239. As the full meet contraction is fully rational, we conclude [2] P. Gärdenfors, Knowledge in flux: Modeling the dy- that the Büchi excerpt effectively accommodates (fully) ra- namics of epistemic states., The MIT press, 1988. tional contraction. [3] S. O. Hansson, A textbook of belief dynamics - theory change and database updating, volume 11 of Applied logic series, Kluwer, 1999. 9. Conclusion [4] C. E. Alchourrón, D. Makinson, On the logic of theory We have investigated the computability of AGM contraction change: Contraction functions and their associated for the class of compendious logics, which embrace several revision functions, Theoria 48 (1982) 14–37. doi:10. logics used in computer science and AI. Due to the high 1111/j.1755-2567.1982.tb00480.x. expressive power of these logics, not all epistemic states [5] P. Gärdenfors, An epistemic approach to conditionals, admit a finite representation. Hence, the epistemic states American Philosophical Quarterly 18 (1981) 203–211. that an agent can assume are confined to a space of theo- [6] S. O. Hansson, Kernel contraction, J. Symb. Log. 59 ries, which depends on a method of finite representation. (1994) 845–859. doi:10.2307/2275912. We have shown a severe negative result: no matter which [7] A. Grove, Two modellings for theory change, J. Philos. form of finite representation we use, as long as it does not Log. 17 (1988) 157–170. doi:10.1007/BF00247909. collapse to the finitary case, AGM contraction suffers from [8] G. Flouris, On Belief Change and Ontology Evolution, uncomputability. Precisely, there are uncountably many Ph.D. thesis, University of Crete, 2006. uncomputable (fully) rational contraction functions in all [9] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduc- such expressive spaces. This negative result also impacts tion to Description Logic, Cambridge University Press, other forms of belief change. For instance, belief revision 2017. is interdefinable with belief contraction, via the Levi Iden- [10] P. Blackburn, J. F. A. K. van Benthem, F. Wolter (Eds.), tity. Therefore, it is likely that revision also suffers from Handbook of Modal Logic, volume 3 of Studies in logic uncomputability. Accordingly, uncomputability might span and practical reasoning, North-Holland, 2007. to iterated belief revision [41], update and erasure [42], and [11] E. M. Clarke, O. Grumberg, D. Kroening, D. A. Peled, pseudo-contraction [43], to cite a few. It is worth investigat- H. Veith, Model checking, 2nd Edition, MIT Press, ing uncomputability of these other operators. 2018. In this work, we have focused on the AGM paradigm, [12] M. M. Ribeiro, R. Wassermann, G. Flouris, G. Antoniou, and logics which are Boolean. We intend to expand our Minimal change: Relevance and recovery revisited, Ar- results for a wider class of logics by dispensing with the tif. Intell. 201 (2013) 59–80. doi:10.1016/J.ARTINT. Boolean operators, and assuming only that the logic is AGM 2013.06.001. compliant. We believe the results shall hold in the more [13] J. P. Delgrande, P. Peppas, Belief revision in Horn general case, as our negative results follow from cardinal- theories, Artif. Intell. 218 (2015) 1–22. doi:10.1016/ ity arguments. On the other hand, several logics used in J.ARTINT.2014.08.006. knowledge representation and reasoning are not AGM com- [14] J. P. Delgrande, R. Wassermann, Horn clause contrac- pliant, as for instance a variety of Description Logics [12]. tion functions: Belief set and belief base approaches, In these logics, the recovery postulate (K− in: KR, AAAI Press, 2010. 5 ) can be replaced by the relevance postulate [44], and contraction functions [15] R. Booth, T. Meyer, I. Varzinczak, R. Wassermann, On the link between partial meet, kernel, and infra telligent Systems, Springer, 2018. doi:10.1007/ contraction and its application to Horn logic, CoRR 978-3-319-60535-7. abs/1401.3902 (2014). arXiv:1401.3902. [32] J. S. Ribeiro, A. Nayak, R. Wassermann, Belief change [16] N. C. da Costa, O. Bueno, Belief change and inconsis- and non-monotonic reasoning sans compactness, in: tency, Logique et Analyse 41 (1998) 31–56. AAAI, AAAI Press, 2019, pp. 3019–3026. doi:10.1609/ [17] M. M. Ribeiro, R. Wassermann, Base revision for on- AAAI.V33I01.33013019. tology debugging, J. Log. Comput. 19 (2009) 721–743. [33] S. O. Hansson, Descriptor Revision: Belief Change doi:10.1093/LOGCOM/EXN048. Through Direct Choice, volume 46, Springer, 2017. [18] J. S. Ribeiro, A. Nayak, R. Wassermann, Towards belief [34] S. O. Hansson, Finite contractions on infinite belief contraction without compactness, in: KR, AAAI Press, sets, Stud Logica 100 (2012) 907–920. doi:10.1007/ 2018, pp. 287–296. S11225-012-9440-9. [19] R. Wassermann, On AGM for non-classical log- [35] B. Nebel, Reasoning and Revision in Hybrid Rep- ics, J. Philos. Log. 40 (2011) 271–294. doi:10.1007/ resentation Systems, volume 422 of Lecture Notes S10992-011-9178-2. in Computer Science, Springer, 1990. doi:10.1007/ [20] B. Nebel, How Hard is it to Revise a Belief Base?, BFB0016445. Springer Netherlands, 1998, pp. 77–145. [36] M. Dalal, Investigations into a theory of knowledge [21] T. Eiter, G. Gottlob, On the complexity of proposi- base revision, in: AAAI, AAAI Press / The MIT Press, tional knowledge base revision, updates, and counter- 1988, pp. 475–479. factuals, Artif. Intell. 57 (1992) 227–270. doi:10.1016/ [37] S. E. Dixon, Belief revision: A computational approach, 0004-3702(92)90018-S. Ph.D. thesis, University of Sydney, 1994. [22] N. Schwind, S. Konieczny, J. Lagniez, P. Marquis, On [38] H. van Ditmarsch, W. van Der Hoek, B. Kooi, Dynamic computational aspects of iterated belief change, in: epistemic logic, volume 337, Springer Science & Busi- IJCAI, ijcai.org, 2020, pp. 1770–1776. doi:10.24963/ ness Media, 2007. IJCAI.2020/245. [39] A. Baltag, L. S. Moss, S. Solecki, The logic of public [23] J. Richard Büchi, Symposium on Decision Problems: announcements and common knowledge and private On a Decision Method in Restricted Second Order suspicions, in: TARK, Morgan Kaufmann, 1998, pp. Arithmetic, volume 44 of Studies in Logic and the 43–56. Foundations of Mathematics, Elsevier, 1966, pp. 1–11. [40] P. Wolper, Temporal logic can be more expres- doi:10.1016/S0049-237X(09)70564-6. sive, Inf. Control. 56 (1983) 72–99. doi:10.1016/ [24] W. M. P. van der Aalst, M. Pesic, H. Schonenberg, S0019-9958(83)80051-5. Declarative workflows: Balancing between flexibility [41] A. Darwiche, J. Pearl, On the logic of iterated belief and support, Comput. Sci. Res. Dev. 23 (2009) 99–113. revision, Artif. Intell. 89 (1997) 1–29. doi:10.1016/ doi:10.1007/S00450-009-0057-9. S0004-3702(96)00038-0. [25] S. Cerrito, M. C. Mayer, Bounded model search in lin- [42] H. Katsuno, A. O. Mendelzon, On the difference be- ear temporal logic and its application to planning, in: tween updating a knowledge base and revising it, in: TABLEAUX, volume 1397 of Lecture Notes in Computer P. Gärdenfors (Ed.), Belief revision, 2003, pp. 183–203. Science, Springer, 1998, pp. 124–140. doi:10.1007/ [43] S. O. Hansson, Changes of disjunctively closed bases, 3-540-69778-0\_18. J. Log. Lang. Inf. 2 (1993) 255–284. doi:10.1007/ [26] G. D. Giacomo, M. Y. Vardi, Automata-theoretic ap- BF01181682. proach to planning for temporally extended goals, [44] S. O. Hansson, Belief contraction without recov- in: ECP, volume 1809 of Lecture Notes in Computer ery, Stud Logica 50 (1991) 251–260. doi:10.1007/ Science, Springer, 1999, pp. 226–238. doi:10.1007/ BF00370186. 10720246\_18. [45] P. T. Guerra, R. Wassermann, Two AGM-style charac- [27] V. Gutiérrez-Basulto, J. C. Jung, A. Ozaki, On met- terizations of model repair, in: KR, AAAI Press, 2018, ric temporal description logics, in: ECAI, volume pp. 645–646. 285 of Frontiers in Artificial Intelligence and Appli- [46] O. Kupferman, M. Y. Vardi, P. Wolper, An automata- cations, IOS Press, 2016, pp. 837–845. doi:10.3233/ theoretic approach to branching-time model check- 978-1-61499-672-9-837. ing, J. ACM 47 (2000) 312–360. doi:10.1145/333979. [28] V. Gutiérrez-Basulto, J. C. Jung, T. Schneider, 333987. Lightweight temporal description logics with rigid [47] J. Hladik, R. Peñaloza, PSPACE automata for descrip- roles and restricted TBoxes, in: IJCAI, AAAI Press, tion logics, in: Description Logics, volume 189 of 2015, pp. 3015–3021. CEUR Workshop Proceedings, CEUR-WS.org, 2006. [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. Geffner, 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 - In- troduction and Overview, Springer Briefs in In-