An axiomatic characterization of temporalised belief revision in the law

Abstract

This paper presents a belief revision operator that considers time intervals for modelling norm change in the law. This approach relates techniques from belief revision formalisms and time intervals with temporalised rules for legal systems. Our goal is to formalise a temporalised belief base and corresponding timed derivation, together with a proper revision operator. This operator may remove rules when needed or adapt intervals of time when contradictory norms are added in the system. For the operator, both constructive definition and an axiomatic characterisation by representation theorems are given.

This is a preview of subscription content, log in to check access.

References

  1. Alchourrón CE, Bulygin E (1981) The expressive conception of norms. In: Hilpinen R (ed), New studies in deontic logic, pp 95–125. D. Reidel, Dordrecht

    Google Scholar 

  2. Alchourrón Carlos E, Gärdenfors Peter, Makinson David C (1985) On the logic of theory change: partial meet contraction and revision functions. J Symb Logic 50:510–530

    MathSciNet  Article  Google Scholar 

  3. Alchourrón CE, Makinson DC (1981) Hierarchies of regulations and their logic. In: Risto H (ed) New studies in deontic logic, pp 125–148. D. Reidel, Dordrecht

    Google Scholar 

  4. Alchourrón CE, Makinson David C (1982) The logic of theory change: contraction functions and their associated revision functions. Theoria 48:14–37

    MathSciNet  Article  Google Scholar 

  5. Alchourrón CE, Makinson David C (1985) On the logic of theory change: safe contraction. Studia Logica 44:405–422

    MathSciNet  Article  Google Scholar 

  6. Allen James F (1983) Maintaining knowledge about temporal intervals. Commun ACM 26(11):832–843

    Article  Google Scholar 

  7. Allen James F (1984) Towards a general theory of action and time. Artif Intell 23(2):123–154

    Article  Google Scholar 

  8. Augusto JC, Simari Guillermo R (2001) Temporal defeasible reasoning. Knowl Inf Syst 3(3):287–318

    Article  Google Scholar 

  9. Boella G, Pigozzi G, Van Der Torre L (2009) A normative framework for norm change. In: Proc. AAMAS 2009, pp 169–176. ACM

  10. Bonanno Giacomo (2007) Axiomatic characterization of the AGM theory of belief revision in a temporal logic. Artif Intell 171(2–3):144–160

    MathSciNet  Article  Google Scholar 

  11. Bonanno G (2009) Belief revision in a temporal framework. In: New perspectives on games and interaction, volume 4 of texts in logic and games, pp 45–80. University Press, Amsterdam

  12. Budán MC, Cobo ML, Marténez DC, Simari Guillermo R (2017) Bipolarity in temporal argumentation frameworks. Int J Approx Reason 84:1–22

    MathSciNet  Article  Google Scholar 

  13. Fuhrmann André (1991) Theory contraction through base contraction. J Philos Logic 20(2):175–203

    MathSciNet  Article  Google Scholar 

  14. Gabbay Dov M, Pigozzi Gabriella, Woods John (2003) Controlled revision—an algorithmic approach for belief revision. J Log Comput 13(1):3–22

    MathSciNet  Article  Google Scholar 

  15. Governatori G, Palmirani M, Riveret R, Rotolo A, Sartor G (2005) Norm modifications in defeasible logic. In: Legal knowledge and information systems—JURIX 2005: the eighteenth annual conference on legal knowledge and information systems, Brussels, Belgium, 8–10 December 2005, pp 13–22

  16. Governatori G, Palmirani M, Riveret R, Rotolo A, Sartor G (2005) Norm modifications in defeasible logic. In: JURIX 2005, pp 13–22. IOS Press, Amsterdam

  17. Governatori G, Rotolo Antonino (2010) Changing legal systems: legal abrogations and annulments in defeasible logic. Logic J IGPL 18(1):157–194

    MathSciNet  Article  Google Scholar 

  18. Governatori Guido, Rotolo Antonino (2015) Logics for legal dynamics. In: Logic in the theory and practice of lawmaking, pp 323–356

    Google Scholar 

  19. Governatori G, Rotolo A, Olivieri F, Scannapieco S (2013) Legal contractions: a logical analysis. In: Proc. ICAIL 2013

  20. Governatori G, Rotolo A, Riveret R, Palmirani M, Sartor G (2007) Variants of temporal defeasible logic for modelling norm modifications. In: Proc. ICAIL’07, pp 155–159

  21. Governatori G, Rotolo A, Sartor G (2005) Temporalised normative positions in defeasible logic. In: Proc. ICAIL 2005

  22. Governatori G, Terenziani P (2007) Temporal extensions to defeasible logic. In: Mehmet AO, John T (eds) AI 2007, Lecture notes in computer science, vol 4830. Springer, Berlin, pp 476–485

    Google Scholar 

  23. Halpern Joseph, Shoham Yoav (1991) A propositional modal logic of time intervals. J ACM 38(4):935–962

    MathSciNet  Article  Google Scholar 

  24. Hansson Sven O (1992) In defense of base contraction. Syntheses 91(3):239–245

    MathSciNet  Article  Google Scholar 

  25. Hansson Sven O (1994) Kernel contraction. J Symb Logic 59:845–859

    MathSciNet  Article  Google Scholar 

  26. Hansson Sven O (1999) A textbook of belief dynamics: theory change and database updating. Kluwer Academic Publishers, Dordrecht

    Google Scholar 

  27. Hart HLA (1994) The concept of law. Clarendon Press, Oxford

    Google Scholar 

  28. Kelsen Hans (1991) General theory of norms. Clarendon, Oxford

    Google Scholar 

  29. Monica Della D, Goranko V, Montanari A, Sciavicco G (2011) Interval temporal logics: a journey. Bull Eur Assoc Theor Comput Sci EATCS 105:01

    MathSciNet  MATH  Google Scholar 

  30. Rotolo A (2010) Retroactive legal changes and revision theory in defeasible logic. In: Governatori G, Sartor G (eds) DEON 2010, volume 6181 of LNAI. LNAI. Springer, Berlin, pp 116–131

    Google Scholar 

  31. Shapiro S, Pagnucco M, Lesprance Y, Levesque HJ (2011) Iterated belief change in the situation calculus. Artif Intell 175(1):165–192. John McCarthy’s Legacy

    MathSciNet  Article  Google Scholar 

  32. Stolpe Audun (2010) Norm-system revision: theory and application. Artif Intell Law 18(3):247–283

    Article  Google Scholar 

  33. Tamargo LH, Martinez DC, Rotolo A, Governatori G (2017) Temporalised belief revision in the law. In: Wyner AZ, Casini G (eds) Legal knowledge and information systems - JURIX 2017: the thirtieth annual conference, Frontiers in artifcial intelligence and applications, vol. 302, Luxembourg, IOS Press, pp 49–58

  34. Wassermann R (2000) Resource bounded belief revision. Ph.D. Thesis, Institute for Logic, Language and Computation (ILLC). University of Amsterdam

  35. Wheeler GR, Alberti M (2011) No revision and no contraction. Minds Mach 21(3):411–430

    Article  Google Scholar 

Download references

Acknowledgements

A preliminary version of this work was published in the proceedings of JURIX 2017 (Tamargo et al. 2017). We would like to thank the anonymous reviewers of JURIX 2017 and the conference audience for their useful comments. This work was partially supported by PGI-UNS (Grants 24/ZN30, 24/ZN32) and EU H2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No. 690974 for the project MIREL: MIning and REasoning with Legal texts.

Author information

Affiliations

Authors

Corresponding author

Correspondence to Luciano H. Tamargo.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Appendix

Appendix

Theorem 1 An operator \(\otimes\) is a prioritised legal revision for \({\mathbb {K}}\) if and only if it satisfies the postulates of (TBR-1) Success, (TBR-2) Inclusion, (TBR-3) Consistency, (TBR-4) Uniformity, and (TBR-5) Safe Retainment.

Proof

Proof has two parts. First, we start from the satisfaction of postulates to the construction as a legal revision operator. Second, we prove that an operator is a legal revision if previous postulates are satisfied.

\(\underline{\Leftarrow )~\hbox {Postulates~to~construction}:}\)

Let \(*\) be an operator that satisfies Success, Inclusion, Consistency, Uniformity and Safe Retainment. We have to show that \(*\) is a legal revision operator.

  1. (1)

    Let \(\sigma ^{c}\) be a function such that for every temporalised base \({\mathbb {K}}\) and for every temporalised sentence \(\alpha ^{J}\) holds \(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})) = {\mathbb {K}} \setminus {\mathbb {K}} * \alpha ^{J}\).

\(\square\)

We first show that \(\sigma ^{c}\) is an incision function. To do this we show that the conditions in Definition 9 are satisfied by \(\sigma ^{c}\); that is:

  • \(\sigma ^{c}\) is a well-defined function: if \(\lnot \alpha ^{J}\) and \(\lnot \beta ^{J}\) are such that \(\varPi (\lnot \alpha ^{J},{\mathbb {K}}) = \varPi (\lnot \beta ^{J},{\mathbb {K}})\) then \(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})) = \sigma ^{c}(\varPi (\lnot \beta ^{J},{\mathbb {K}}))\).

    Let \(\lnot \alpha ^{J}\) and \(\lnot \beta ^{J}\) be two temporalised sentences such that \(\varPi (\lnot \alpha ^{J},{\mathbb {K}}) = \varPi (\lnot \beta ^{J},{\mathbb {K}})\). We need to show that \(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})) = \sigma ^{c}(\varPi (\lnot \beta ^{J},{\mathbb {K}}))\). By Definition 6 and Definition 5, for all subset \({\mathbb {K}} '\) of \({\mathbb {K}}\), \(\lnot \alpha ^{J} \in Cn^t({\mathbb {K}} ')\) if and only if \(\lnot \beta ^{J} \in Cn^t({\mathbb {K}} ')\). Then \(\lnot \alpha ^{J} \cup {\mathbb {K}} '\) is temporally inconsistent if and only if \(\lnot \beta ^{J} \cup {\mathbb {K}} '\) is temporally inconsistent. Thus, by uniformity, \({\mathbb {K}} \cap ({\mathbb {K}} *\alpha ^{J}) = {\mathbb {K}} \cap ({\mathbb {K}} *\beta ^{J})\). Then, \({\mathbb {K}} \setminus ({\mathbb {K}} *\alpha ^{J}) = {\mathbb {K}} \setminus ({\mathbb {K}} *\beta ^{J})\). Therefore, by (1), \(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})) = \sigma ^{c}(\varPi (\lnot \beta ^{J},{\mathbb {K}}))\).

  • \(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})) \subseteq \bigcup (\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\).

    Let \(\beta ^{P} \in \sigma (\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\). By (1), we have that \(\beta ^{P} \in {\mathbb {K}} \setminus {\mathbb {K}} *\alpha ^{J}\). Then, it holds that \(\beta ^{P} \not \in {\mathbb {K}} *\alpha ^{J}\), and from \({\textit{Safe Retainment}}\) we have that \(\beta ^{P}\) is not a safe element, otherwise it will be part of the revision. Since \(\beta ^{P}\) is not a safe element then it holds that \(\beta ^{P}\) is a sentence that can produce effects in favour of a possible temporal contradiction with \(\alpha ^{J}\) where J and P are overlapped time interval. Then, \(\beta ^{P}\) is in a minimal subset (under set inclusion) \({\mathbb {H}}\) of \({\mathbb {K}}\) such that \({\mathbb {H}} \cup \alpha ^{J}\) is temporally inconsistent. By Definition 6, if \({\mathbb {H}}\) is a minimal subset such that \({\mathbb {H}} \cup \alpha ^{J}\) is temporally inconsistent then \({\mathbb {H}} \in \varPi (\lnot \alpha ^{J},{\mathbb {K}})\), and therefore \(\beta ^{P} \in \bigcup (\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\). Since this holds for any arbitrary \(\beta ^{P} \in \sigma (\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\) we have that \(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})) \subseteq \bigcup (\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\).

  • If \({\mathbb {H}} \in \varPi (\alpha ^{J},{\mathbb {K}})\), \({\mathbb {H}} \cap \sigma ^{c}(\varPi (\alpha ^{J},{\mathbb {K}})) \ne \emptyset\).

    Let \({\mathbb {H}} \in \varPi (\alpha ^{J},{\mathbb {K}})\). We need to show that \({\mathbb {H}} \cap \sigma ^{c}(\varPi (\alpha ^{J},{\mathbb {K}})) \ne \emptyset\). We should prove that, there exists \(\beta ^{P} \in {\mathbb {H}}\) such that \(\beta ^{P} \in \sigma ^{c}(\varPi (\alpha ^{J},{\mathbb {K}}))\). Suppose \(\lnot \alpha ^{J}\) is consistent. Since we have assumed that \({\mathbb {K}}\) is temporally consistent, by consistency, \({\mathbb {K}} *\lnot \alpha ^{J}\) is temporally consistent. Since \({\mathbb {H}}\) is inconsistent with \(\lnot \alpha ^{J}\) then \({\mathbb {H}} \not \subseteq {\mathbb {K}} *\lnot \alpha ^{J}\) by success. This means that there is some \(\beta ^{P} \in {\mathbb {H}}\) and \(\beta ^{P} \not \in {\mathbb {K}} *\lnot \alpha ^{J}\). Since \({\mathbb {H}} \subseteq {\mathbb {K}}\) it follows that \(\beta ^{P} \in {\mathbb {K}} \setminus {\mathbb {K}} *\lnot \alpha ^{J}\); i.e., by our definition of \(\sigma ^{c}\), \(\beta ^{P} \in \sigma ^{c}(\varPi (\alpha ^{J},{\mathbb {K}}))\). Therefore, \({\mathbb {H}} \cap \sigma ^{c}(\varPi (\alpha ^{J},{\mathbb {K}})) \ne \emptyset\).

  • \(\beta ^{P} \in \sigma ^{c}(\varPi (\alpha ^{J},{\mathbb {K}}))\) then for some \({\mathbb {H}} \in \varPi (\alpha ^{J},{\mathbb {K}})\) such that \(\beta ^{P} \in {\mathbb {H}}\) it holds that \(\beta = \alpha\) or \(\beta ^{P} = \delta ^{Q} \rightarrow \alpha ^{P} {\text { and }} \delta \in {\mathbb {L}}\).

    Let \(\beta ^{P} \in \sigma ^{c}(\varPi (\alpha ^{J},{\mathbb {K}}))\). Then \(\beta ^{P} \in {\mathbb {K}} \setminus ({\mathbb {K}} *\lnot \alpha ^{J})\), hence \(\beta ^{P} \not \in {\mathbb {K}} *\lnot \alpha ^{J}\). Therefore, by Safe Retainment we have that \(\beta ^{P}\) is not a safe element. Since \(\beta ^{P}\) is not a safe element then it holds that \(\beta ^{P}\) is a sentence that can produce effects in favour of a possible temporally contradiction with \(\alpha ^{J}\) where J and P are overlapped time interval. Then, \(\beta ^{P}\) is in a minimal subset (under set inclusion) \({\mathbb {H}}\) of \({\mathbb {K}}\) such that \({\mathbb {H}} \cup \alpha ^{J}\) is temporally inconsistent. By Definition 6, if \({\mathbb {H}}\) is a minimal subset such that \({\mathbb {H}} \cup \alpha ^{J}\) is temporally inconsistent then \({\mathbb {H}} \in \varPi (\alpha ^{J},{\mathbb {K}})\). Then, since \(\beta ^{P}\) is a sentence that can produce effects in favour of a possible temporally contradiction with \(\alpha ^{J}\), \(\beta = \alpha\) or \(\beta ^{P} = \delta ^{Q} \rightarrow \alpha ^{P} {\text { and }} \delta \in {\mathbb {L}}\).

Once we have proven that \(\sigma ^{c}\) is a proper incision function, to finalise the proof we must show that \({\mathbb {K}} *\alpha ^{J} = {\mathbb {K}} \otimes \alpha ^{J}\).

(\(\subseteq\)):

Let \(\beta ^{[t_i]} \in {\mathbb {K}} *\alpha ^{J}\).

It follows by inclusion that \(\beta ^{[t_i]} \in {\mathbb {K}} \cup \{\alpha ^{J}\}\).

Then, \(\beta ^{[t_i]} \in {\mathbb {K}}\).

It follows from \(\beta ^{[t_i]} \in {\mathbb {K}} *\alpha ^{J}\) and \(\beta ^{[t_i]} \in {\mathbb {K}}\) that \(\beta ^{[t_i]} \not \in {\mathbb {K}} \setminus {\mathbb {K}} *\alpha ^{J}\).

Thus, by (1), \(\beta ^{[t_i]} \not \in \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\). Hence, \(\beta ^{[t_i]} \in {\mathbb {K}} \otimes \alpha ^{J}\).

(\(\supseteq\)):

Let \(\beta ^{[t_i]} \in {\mathbb {K}} \otimes \alpha ^{J}\).

By definition, \(\beta ^{[t_i]} \in ({\mathbb {K}} \setminus \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))) \cup out(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})),J) \cup \ \{\alpha ^{J}\}\).

From Remark 4, \(out(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})),J) \subseteq {\mathbb {K}}\) and then, \(\beta ^{[t_i]} \in {\mathbb {K}}\) and \(\beta ^{[t_i]} \not \in \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\).

Thus, by (1), \(\beta ^{[t_i]} \not \in {\mathbb {K}} \setminus {\mathbb {K}} *\alpha ^{J}\).

Hence, \(\beta ^{[t_i]} \in {\mathbb {K}} *\alpha ^{J}\).

The second part of the demonstration follows.

\(\Rightarrow )\)Construction to postulates: Let \(\sigma ^{c}\) be a consequence incision function and \(\otimes\) its associated operator and \({\mathbb {K}}\) a knowledge base. Then, for all \(\alpha ^{J}\):

\({\mathbb {K}} \otimes \alpha ^{J}\)\(=\)\(({\mathbb {K}} \setminus S) \cup out(S,J) \cup \ \{\alpha ^{J}\}\) where \(S = \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\).

We prove that the postulates hold for the given construction, as follows.

  • Success\(\alpha ^{J} \in {\mathbb {K}} \otimes \alpha ^{J}\).

    Straightforward by Definition 11.

  • Inclusion If \(\beta ^{[t_i]} \in {\mathbb {K}} \otimes \alpha ^{J}\) then \(\beta ^{[t_i]} \in {\mathbb {K}} \cup \{\alpha ^{J}\}\).

    Let \(\beta ^{[t_i]} \in {\mathbb {K}} \otimes \alpha ^{J}\). From Definition 11 we have that \({\mathbb {K}} \otimes \alpha ^{J}\)\(=\)\(({\mathbb {K}} \setminus S) \cup out(S,J) \cup \ \{\alpha ^{J}\}\) where \(S = \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\). Following Remark 4, for all \(\beta ^{P} \in S\) there exists \(\beta ^{Q} \in out(S,J)\) such that \(Q \subseteq P\). Then, \(out(S,J) \subseteq {\mathbb {K}}\). Therefore, \(\beta ^{[t_i]} \in {\mathbb {K}} \cup \{\alpha ^{J}\}\).

  • Consistence if \(\alpha ^{J}\) is consistent then \({\mathbb {K}} \otimes \alpha ^{J}\) is temporally consistent.

    Suppose \(\alpha\) is consistent. By Definition 8, \(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\) returns a set of sentences which they are selected from every subset of \({\mathbb {K}}\) temporally inconsistent with \(\alpha ^{J}\). Then, since \({\mathbb {K}}\) is temporally consistent (Remark 1), \({\mathbb {K}} \setminus \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\) is temporally consistent. From Definition 10, if there exists \(\lnot \alpha ^{Q}\) or \(\beta ^{P} \rightarrow \alpha ^{Q}\) in \(out(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})),J)\) then the intervals J and Q are not overlapped. Therefore, \({\mathbb {K}} \setminus \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})) \cup out(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})),J)\) is temporally consistent. Then, following Definition 11, \({\mathbb {K}} \otimes \alpha ^{J}\) is temporally consistent.

  • Uniformity if for all \({\mathbb {K}} ' \subseteq {\mathbb {K}}\), \(\{\alpha ^{J}\} \cup {\mathbb {K}} '\) is temporally inconsistent if and only if \(\{\beta ^{J}\} \cup {\mathbb {K}} '\) is temporally inconsistent then \({\mathbb {K}} \cap ({\mathbb {K}} \otimes \alpha ^{J}) = {\mathbb {K}} \cap ({\mathbb {K}} \otimes \beta ^{J})\).

    Let \(\alpha\) and \(\beta\) be consistent sentences and J a time interval. Suppose that for all subset \({\mathbb {K}}\) ’ of \({\mathbb {K}}\), \(\{\alpha ^{J}\} \cup {\mathbb {K}} '\) is temporally inconsistent if and only if \(\{\beta ^{J}\} \cup {\mathbb {K}} '\) is temporally inconsistent. Then \(\varPi (\alpha ^{J},{\mathbb {K}}) = \varPi (\beta ^{J},{\mathbb {K}})\) and since \(\sigma ^{c}\) is a well defined function then \(\sigma ^{c}(\varPi (\alpha ^{J},{\mathbb {K}})) = \sigma ^{c}(\varPi (\beta ^{J},{\mathbb {K}}))\). In the same way \(out(\sigma ^{c}(\varPi (\alpha ^{J},{\mathbb {K}})),J) = out(\sigma ^{c}(\varPi (\beta ^{J},{\mathbb {K}})),J)\). Therefore, \({\mathbb {K}} \cap ({\mathbb {K}} \otimes \alpha ^{J}) = {\mathbb {K}} \cap ({\mathbb {K}} \otimes \beta ^{J})\).

  • Safe retaiment\(\beta ^{P} \in {\mathbb {K}} \otimes \alpha ^{J}\) if and only if \(\beta ^{P}\) is a safe element with respect to \(\alpha ^{J}\) in \({\mathbb {K}}\).

    • Proof that if \(\beta ^{P} \in {\mathbb {K}} \otimes \alpha ^{J}\) then \(\beta ^{P}\) is a safe element with respect to \(\alpha ^{J}\) in \({\mathbb {K}}\).

      Let \(\beta ^{P} \in {\mathbb {K}} \otimes \alpha ^{J}\) then by Definition 11 we have two alternatives:

      • \(\beta ^{P} \not \in \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\). We can identify two different cases: either \(\beta ^{P}\) does not belong to any minimal proof, or it does. Let us consider the two cases separately.

        If \(\beta ^{P}\not \in X\) for every \(X \in \varPi (\lnot \alpha ^{{\mathbb {K}}},J)\) then \(\lnot \alpha ^{J}\) does not belong to any minimal set (under set inclusion) B of \({\mathbb {K}}\) such that \(\lnot \alpha ^{Q} \in Cn^t(B)\) with \(J \top Q\) and then it is a safe element with respect to \(\alpha ^{J}\) in \({\mathbb {K}}\).

        Now consider the case where \(\beta ^{P} \in X\) for every \(X \in \varPi (\lnot \alpha ^{{\mathbb {K}}},J)\). Since \(\beta ^{P} \not \in \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\) then by Definition 9 and Definition 8, \(\beta \ne \alpha\) and \(\beta \ne \delta \rightarrow \alpha\). Then \(\beta ^{P}\) is not a sentence that can produce effects in favour of a possible temporally contradiction with \(\alpha ^{J}\). Hence, \(\beta ^{P}\) is a safe element with respect to \(\alpha ^{J}\) in \({\mathbb {K}}\).

      • \(\beta ^{P} \in \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\). Since \(\beta ^{P} \in {\mathbb {K}} \otimes \alpha ^{J}\) then, by Definition 11, \(\beta ^{P} \in out(\sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}})),J)\). Then, by Definition 10, the time intervals P and J are not overlapped. Therefore, \(\beta ^{P}\) is a safe element with respect to \(\alpha ^{J}\) in \({\mathbb {K}}\).

    • Proof that if \(\beta ^{P}\) is a safe element with respect to \(\alpha ^{J}\) in K then \(\beta ^{P} \in {\mathbb {K}} \otimes \alpha ^{J}\).

      Let \(\beta ^{P} \in {\mathbb {K}}\) be a safe element with respect to the revision of \({\mathbb {K}}\) by \(\alpha ^{J}\). Then, \(\beta ^{P}\) is not a sentence that can produce effects in favour of a possible temporally contradiction with \(\alpha ^{J}\) where J and P are overlapped time interval. Then, \(\beta ^{P}\) does not belong to any minimal subset under set inclusion X of \({\mathbb {K}}\) such that \(\lnot \alpha ^{J} \in Cn^t(X)\) with \(J \top P\). Thus, by Definition 6, \(\beta ^{P} \not \in \bigcup (\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\). Following Definition 9, \(\beta ^{P} \not \in \sigma ^{c}(\varPi (\lnot \alpha ^{J},{\mathbb {K}}))\). Therefore, by Definition 11, \(\beta ^{P} \in {\mathbb {K}} \otimes \alpha ^{J}\).

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Tamargo, L.H., Martinez, D.C., Rotolo, A. et al. An axiomatic characterization of temporalised belief revision in the law. Artif Intell Law 27, 347–367 (2019). https://doi.org/10.1007/s10506-019-09241-4

Download citation

Keywords

  • Norm change
  • Belief revision
  • Temporal reasoning