In the logic of theory change, the AGM model has acquired the status of a standard model. However, the AGM model does not seem adequate for some contexts and application domains. This inspired many researchers to propose extensions and generalizations to AGM. Among these extensions, one of the most important are belief bases. Belief bases have more expressivity than belief sets, as explicit and implicit beliefs have diferent statuses. In this paper, we present reformulation, a belief change operation that allows us to reformulate a belief base making some particular sentences explicit without modifying the consequences of the belief base. We provide a constructive method and its axiomatic characterization.
The primary objective of the area of belief change is to identify appropriate methods for modeling
belief states of rational agents and the changes that occur in these states when the agent receives new
information as a result of its interaction with the world. One of the most significant extensions to the
seminal work of AGM [
It can be considered thus, that while 1 and 2 are statically equivalent, they fail to be dynamically
equivalent [
Before outlining the technical details of our proposal, consider the next example in the legal domain. Assume the proposition states that “Users under 18 cannot enter into binding contracts” and the sentences ↔ states that “Users that are not able to enter binding contracts means do not have full legal capacity”. Now, assume we have the following belief base = {, ↔ }. From we can infer that : “Under-18s do not have full legal capacity”, however, if the rules change and certain exceptions for 16-17 years-olds are allowed (for instance by obtaining parent’s consent), the revision of by this new information may create undesired efects. Since q is implicit, the revision mechanism might attempt to accommodate the new rule by altering or even discarding ↔ or by weakening . This creates ambiguity: do 16–17 year-olds with parental consent have full legal capacity, or is legal capacity still tied to minority status? On the other hand, an operator that makes explicit first can act as a “clarifier”, preserving the rules’ consequences while improving clarity, usability, and allowing for more transparent change operations.
First, we recall the two well-known constructive models of contraction functions on belief bases as we
our proposal aims to exploit these well-known operators as the basis for the contruction of the new one.
Definition 1 (Partial meet base contraction [
An operation − on is a partial meet contraction if and only if there is a selection function for such that for all sentences : − = − .
Definition 2 (Kernel base contraction [
Definition 3 (Reformulation). Let be a belief base, a formula, and − a base contraction function. The reformulation of in is:
(, ) = − ∪ { → : ̸⊢ ↔ and ∈ ∖ − } ∪ {} when ⊢ , and (, ) = when ̸⊢ .
Note that in the definition above, − can be any belief base contraction function. If − is a partial meet base contraction then (, ) is a partial meet-based reformulation operation, and if − is a kernel base contraction then (, ) is a kernel-based reformulation operation.
Basically, the operation eliminates all the implicit ways to obtain from the belief base via a contraction function and adds explicitly. All the explicit sentences that were erased in the contraction can be recovered, implicitly, thanks to the addition of { → : ̸⊢ ↔ and ∈ ∖ − }. 2.1. Postulates for Reformulation In this section we introduce postulates that constitute desirable properties of reformulation operations. In addition to (R1), the following are a set of minimum requirements. (R2) If ⊢ , then ∈ (, ). (Explicit Success) (R2b) If ̸⊢ then (, ) ∖ {} ̸⊢ . (R3) If ∈ and ̸∈ (, ), then there exists such that ⊆ and ( ∩ (, )) ∖ {} ⊆ and ̸⊢ but ∪ {} ⊢ . (Relevance) (R5) If ∈ and ̸∈ (, ), then there exists ⊆ such that ̸⊢ but ∪ {} ⊢ . (Core-retainment) (R4) If ∈ (′) if and only if ∈ (′) for all subsets ′ of , then ∩ ((, ) ∖ {, }) = ∩ ((, ) ∖ {, }). (Uniformity) (R6) If ∈ ∖ (, ), then → ∈ (, ). (Recovery) (R6b) If ∈ (, ) ∖ ( ∪ {}), then there exists such that ∈ ∖ (, ) and ⊢ ↔ ( → ). (Dual Recovery)
The postulates above resemble those that characterize contraction operations. The main diference is
that the reformulation operator aims to reorganize the belief base by making a sentence explicit but
the inferences of the original base must remain. Explicit and isolation success ensure that is made
exclusively explicit, while 3 (5) and 6 (6) ensure that only knowledge that implicitly infers is
removed. Finally, 4 ensures that the result of reformulating by depends only on which subsets of
imply some element of ; that is, if two sentences have the same epistemic attitude regarding all the
subsets of , then their reformulations coincide (with the exception of the proper sentences).
Representation Theorems: In the full paper [
In [
2 (, ) = − ∪ {} ∪ { → : ∈ ∖ − and− ̸⊢ → } when ⊢ , and 2 (, ) = when ̸⊢ .
The aim of this paper was to introduce an operation that reformulates a belief base by making explicit a particular sentence that was originally implicit. Such an operation had not been investigated before in the theory of belief base change operations. We have defined this operation of reformulation in terms of a base contraction operator. We have studied its axiomatic characterization in two versions that are respectively based on partial meet contraction and kernel base contraction. We have also proposed three alternatives that further refine reformulation and that enhance non-redundancy. The precise axiomatic characterization for these alternatives is left to future work. MVM was partially supported by the Spanish project PID 2022-139835NB-C21 funded by MCIN/AEI/10.13039/501100011033, PIE 2023-5AT010 and iTrust (PCI 2022-135010-2) CHIST-ERA under grant 2022/04/Y/ST6/00001. EF was partially supported by FCT-Fundação para a Ciência e a Tecnologia, Portugal, through project PTDC/CCI-COM/4464/2020 and by NOVA LINCS ref. UIDB/04516/2020 and ref. UIDP/04516/2020 with the financial support of FCT.IP. https://doi.org/10.54499/UIDP/04516/2020.