Paper deep dive
Obligation-Producing Actions
Kalonji Kalala, Iluju Kiringa, Tet Yeap
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%
Last extracted: 7/9/2026, 5:42:57 AM
Summary
This paper formalizes obligation-producing actions within Reiter's Situation Calculus to address the frame problem in deontic reasoning. It introduces a deontic accessibility relation to model obligations, simplifying prior work by removing situation ideality and aligning with Kripke-style possible-world semantics. The authors extend successor state axioms and the regression operator to handle obligations, enabling precise specification and automated reasoning for smart legal contracts and dynamic multi-agent systems.
Entities (9)
Relation Signals (8)
Obligation-Producing Actions โ generates โ Obligations
confidence 95% ยท actions that create obligations on the part of the agent that performs them
Raymond Reiter โ proposed โ Successor State Axioms
confidence 95% ยท Raymond Reiterโs solution to the frame problem... proposed the so-called successor state axioms
Obligation-Producing Actions โ modeledvia โ Accessibility Relation
confidence 90% ยท affect the truth value of a newly introduced fluent that captures the accessibility relation used in semantics of obligation modalities
Situation Calculus โ solves โ Frame Problem
confidence 90% ยท Situation Calculus... solution to the frame problem for actions that change the external world
Successor State Axioms โ solves โ Frame Problem
confidence 90% ยท proposed the so-called successor state axioms as a solution to the frame problem
Accessibility Relation โ basedon โ Kripke-style Possible-World Semantics
confidence 85% ยท remaining close to Kripke-style possible-world semantics for deontic logic, in the spirit of Governatori's approach
Smart Legal Contracts โ requires โ Formal Obligation Reasoning
confidence 85% ยท enable the precise specification and automated reasoning of legal documents and smart legal contracts
Demolombe โ extended โ
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:This paper proposes a Situation Calculus solution to the frame problem for obligation-producing actions, which are actions that create obligations on the part of the agent that performs them. As an example of such actions, we have an opening door action performed by an agent, which has the subsequent obligation of getting the door closed. Demolombe and others extend Raymond Reiter's solution to the frame problem for ordinary actions to accommodate obligation-producing actions. Obligation-producing actions do affect the truth value of a newly introduced fluent that captures the accessibility relation used in semantics of obligation modalities in the Situation Calculus. Our work simplifies Demolombe's characterization of the accessibility relation by eliminating the notion of ideality of situations, thereby remaining close to Kripke-style possible-world semantics for deontic logic, in the spirit of Governatori's approach. Furthermore, we spell out details of a complete solution by extending basic action theories of Reiter to the new setting. Finally, we extend Reiter's regression operator for reasoning about actions back to the initial situation to this new setting. Our solution yields intuitive properties that one would expect from obligations: for example, if a sentence is obligatory to an agent in a given situation, it remains so in subsequent situations unless the obligation is explicitly stopped.
Tags
Links
- Source: https://arxiv.org/abs/2606.14810v1
- Canonical: https://arxiv.org/abs/2606.14810v1
Trouble viewing inline? Open PDF directly โ
Full Text
58,596 characters extracted from source content.
Expand or collapse full text
Obligation-Producing Actions in Situation Calculus Kalonji Kalala โ hkalo081@uottawa.ca University of Ottawa Ottawa, Ontario, Canada Iluju Kiringa iluju.kiringa@uottawa.ca University of Ottawa Ottawa, Ontario, Canada Tet Yeap tyeap@uottawa.ca University of Ottawa Ottawa, Ontario, Canada Abstract This paper proposes a Situation Calculus solution to the frame problem for obligation-producing actions which are actions that create obligations on the part of the agent that performs them. As an example of such actions, we have an opening door action per- formed by an agent which has the subsequent obligation of getting the door closed. Demolombe and others extend Raymond Reiterโs solution to the frame problem for ordinary actions to accommo- date obligation-producing actions. Obligation-producing actions do affect the truth value of a newly introduced fluent that captures the accessibility relation used in semantics of obligation modalities in the Situation Calculus. Our work simplifies Demolombeโs char- acterization of the accessibility relation by eliminating the notion of ideality of situations, thereby remaining close to Kripke-style possible-world semantics for deontic logic, in the spirit of Gover- natoriโs approach. Furthermore, we spell out details of a complete solution by extending basic action theories of Reiter to the new setting. Finally, we extend Reiterโs regression operator for reason- ing about actions back to the initial situation to this new setting. Our solution yields intuitive properties that one would expect from obligations: for example, if a sentence is obligatory to an agent in a given situation, it remains so in subsequent situations, unless the obligation is explicitly stopped. CCS Concepts โข Do Not Use This CodeโGenerate the Correct Terms for Your Paper; Generate the Correct Terms for Your Paper; Generate the Correct Terms for Your Paper; Generate the Correct Terms for Your Paper. Keywords Situation Calculus, legal contract, Obligations, Frame Problem, Re- gression, Action, Fluent ACM Reference Format: Kalonji Kalala, Iluju Kiringa, and Tet Yeap. 2018. Obligation-Producing Ac- tions in Situation Calculus. In . Legal Agent Workshop (LAWโ26), Singapore, Singapore, 11 pages. https://doi.org/X.X Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. LAWโ26 Legal Agent Workshop, Singapore, Singapore ยฉ 2018 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 978-x-x-x-x/Y/M https://doi.org/X.X 1 Introduction The Situation Calculus presented in [22] is a logical language that has been used in artificial intelligence for specifying and reasoning about dynamical systems such as robotics, database updates, control systems, and simulated software agents. Axioms are provided to capture the prerequisites of actions of the domain and the effects of these actions on the external world around the specified system. The effects of actions are captured by fluents, predicates whose truth values are changed as the result of the performance of actions. In this context, the challenge of specifying axioms that describe what remains unchanged in a compact way is known as the frame problem in artificial intelligence. The seminal work reported in [29] has proposed the so-called successor state axioms as a solution to the frame problem for actions that change the external world. In [31], authors extend Reiterโs solution to the frame problem to actions that change the state of the knowledge of a reasoning agent; these actions are called knowledge-producing actions. The work in [6] gives the first formulation of Deontic Logic concepts in the Situation Calculus to capture an agentโs set of obligations. The authors use the approach to knowledge from [31] by representing obligations through an appropriate first-order representation of the accessibility relation of the semantics of modal Deontic Logic. This paper extends the ideas found in [6] to a full-fledged so- lution. Demolombe et al. did not develop a complete framework stretching from a logic of obligation-producing actions to reason- ing about these actions and implementing specifications written in the said logic of obligation-producing actions. We go further than the work in [6] by simplifying the formalization to keep it close to the Kripke-style possible world semantics for deontic logic from [13] that was embedded in the Situation Calculus by Scherl and Levesque. We simplify Demolombeโs axiom for characterizing the newly introduced accessibility relation by getting rid of the notion of ideality of situations. Furthermore, we spell out details of a complete solution by extending basic action theories of Reiter to the new setting. In addition, we extend Reiterโs regression opera- tor for reasoning about actions back to the initial situation to this new setting and we extend his regression theorem to obligations. Finally, we show that the formalization yields intuitive properties that one would expect from obligations: for example, if obligatory sentences remain so in subsequent situations, unless the obligation is explicitly stopped. There are two main motivations for formalizing obligations in the Situation Calculus. The first motivation is of a purely scien- tific nature: namely, how to formalize logical modalities within the largely first-order framework of the Situation Calculus. Although this has been accomplished for the epistemic modality of knowl- edge, it remains not yet fully realized for the deontic modality of obligation. The second motivation for formalizing obligations is to enable the precise specification and automated reasoning of legal arXiv:2606.14810v1 [cs.LO] 12 Jun 2026 LAWโ26 Legal Agent Workshop, June 2026, Singapore, SingaporeKalonji Kalala et al. documents and smart legal contracts. A legal contract is a legally enforceable agreement that contains requirements for parties to engage in business transactions [16][21]. A smart contract is the logical implementation of a legal contract. These artifacts have become increasingly prominent in cyber-physical systems, where they serve as mechanisms for enforcing formally defined (and thus obligatory) agreements among interacting entities. By providing a rigid semantic foundation, formal models of obligations support verification, consistency checking, and the reliable execution of such agreements in dynamic and distributed environments (see, e.g., [4]). 2 Formal Background 2.1 Sequential and Temporal Situation Calculus The Situation Calculus [22, 29] is a many-sorted and mostly first order language with equality specifically designed for representing dynamically changing world. We consider a version of the Situation Calculus with four sorts for actions (A), situations (S), time points (T ), and objects (O) other that the first three sorts. Actions are first order terms consisting of an action function sym- bol and its arguments, one of which being the action occurrence time. Named actions are the cause of every change in the world. For example : โข ํขํํํํํ(ํ,ํก): An action that represents the fact of unlocking the door ํ at the time ํก . โข ํํํํ(ํ,ํก) : An action that represents the fact of locking the door ํ at the time ํก . Actions are executed by agents in the domain. Situations are first order terms denoting finite sequences of actions and represented by a binary function symbolํํ:ํํ(ํผ,ํ )denotes the sequence resulting from adding the actionํผto a sequenceํ . ํํ(ํผ,ํ )denotes the successor situation toํ obtained by performing the action ํผ . For example โข ํํ(ํขํํํํํ(ํท, 10),ํ 0 )): Represents the next situation after executing the actionํขํํํํํ(ํท,10)in the situationํ 0 .ํทis a specific door that is unlocked at point time 10. The constantํ 0 (initial situation) denotes the empty sequence[ ] of actions. It is used to indicate the initial situation, which means that there no exists a situation before ํ 0 . Time points: In the temporal Situation Calculus, the history of the world will be represented with the exact duration of time, or the range of times of the actions. Time will be expressed explicitly as a sequence of real numbers. Finally, objects represent domain specific individuals other than actions, situations, and time points. The languageโs alphabet has variables and a finite number of constants for each sort, a finite number of action function symbols, a finite number of situation independent functions, a finite number of functional fluents, which are function symbols with a situation argument, a finite number of situation independent predicates, and a finite number of predicate fluents with a situation argument. Predicate fluents or relational fluents represent properties whose truth values vary from situation to situation as a consequence of executions of actions. A predicate fluent is denoted by a predicate symbol whose last argument is a situation term. For example : โข ํํํํํํ(ํ,ํ ): A relational (predicate) fluent indicating that the agent has locked the door in the situations. The value of the predicate should be True or False. Functional fluents denote values that vary from situation to situ- ation as a consequence of executions of actions. The language also includes special predicatesํํํ , andโ. The pred- icateโ: situationรsituation establishes the relation of order on the situations.ํ โ ํ โฒ states that the situationํ โฒ is reachable from the situationํ by performing some sequence of actions. The predicate symbol Poss: actionรsituation. Poss(a,s) reflects the fact that it is possible to accomplish the action a in situation s. In this approach of axiomatizing legal contract domain into the Situation Calculus, we consider fluents to be used to represent the obligations between parties. The truth value of a such fluent will determine the performing of an obligation. Some actions called obli- gation producing actions are used to produce obligation whoever agent perform them. Inํ 0 all obligations represented by fluents are false. A dynamic domain is axiomatized in the Situation Calculus with axioms which describe how and under what conditions change oc- curs or not as a result of performing actions. Such axioms are called basic action theory in [29], as expressed in the definition 2.1. They include the following classes of sentences: foundational axioms for situations; action precondition axioms stating the conditions of change; successor state axioms stating how change occurs; specific axioms for time, stating the action occurrence times and start times of situations; unique names axioms for action terms; and axioms describing ํ 0 . Definition 2.1. The Basic Action Theories A basic action theories is a set of axiomsํin the form expressed by formula in 1. The formula designates a basic action theory: ํ=ฮฃโชํ ํ โชํ ํํ โชํ ํขํํ โชํ ํ ํ (1) with : โขฮฃ contains the set the four foundational axioms [17]. โขํ ํ contains a collection of successor state axioms. โขํ ํํ contains a collection of actions precondition axioms. โขํ ํขํํ contains unique names axioms for situations . โขํ ํ ํ consists of a collection of first order sentences which are uniform in ํ 0 . ํ 0 represents the initial state of any domain. Our domain is about obligations in legal contract, thus we will have the initial legal contract state. All sentences ofํ ํ ํ only indicate theํ 0 term of sort situation [17]. This because there is not any sentence containing in ํท ํ0 that indicates any do (functional symbol), Poss orโ. 2.2 Frame Problem The frame problem in Artificial Intelligence examines how to rep- resent what remains unchanged after an action without explicitly listing all unaffected facts [12][1]. In formalisms such as Situation Calculus, actions modify some fluents (properties of the world), but the majority of them persist [18][27]. Reasoning becomes ineffec- tive when this is naively encoded since it demands a lot of "frame Obligation-Producing Actions in Situation CalculusLAWโ26 Legal Agent Workshop, June 2026, Singapore, Singapore axioms." This is addressed by solutions like successor state axioms and non-monotonic reasoning, which assume persistence in other situations and only specify when changes take place. In AI systems dealing with law, the frame problem is especially important since legal logic requires tracking how actions alter rights, duties, and rulesโwithout accidentally changing unrelated legal facts. For instance, fulfilling a fine modifies the status of an obligation but shouldnโt modify other contracts or entitlements. When using systems built on deontic logic, itโs crucial to update only the legally relevant effects while keeping the broader legal framework unchanged. Solving this challenge efficiently is key to building trustworthy legal reasoning agents. In this paper, we use successor state axioms in Situation Calculus to handle the frame problem to capture changes that happen, and later on, to be able to build a complete framework to reason about obligations in multi- agent legal systems [7][32]. 2.3 Running Example: Opening a Door We consider a variation of the Mooreโs safe opening example as expressed in [23], with a door replacing a safe. To start, let us enu- merate some of the actions and fluents of the domain. Primitive actions are:ํขํํํํํ(ํ,ํก),ํํํํ(ํ,ํก),ํํํฃํํํ(ํ), and ํํํกํํํฆ(ํ,ํก). Fluents are:ํํํํ(ํ,ํ ),ํํํํํํ(ํ,ํ ),ํํํกํํํํํํํํํํํํ(ํ ),ํํก(ํ,ํ ). Finally, situation independent predicates and function are: ํํํํํํํ(ํ), and ํํํ(ํ). All these actions, fluents, functions, and predicates are intuitively understandable, except the following: Primitive Actions. โข ํํํํ ํตํขํกํํ(ํ,ํธ,ํก): press the button to open the doorํwith credential ํธ at time ํก ; ํธ is a constant meaning "Employee". โข ํํํกํํํฆ(ํ,ํก): notify the managerํof the locking of the door at time ํก . Fluents. โข ํํํํํํ(ํ,ํ ): relational fluent meaning that the agent has locked the door in s. โข ํํํกํํํํํํํํํํํํ(ํ ): functional fluent meaning the man- ager has been notified of the locking of the door. โข ํํก(ํ,ํ ): the agent is at the door ํ in situation ํ . โข ํํํํ(ํ,ํ ) : relational fluent meaning that the agent has open the door d in s. Action Precondition Axioms. There is one for each action func- tion ํด(ยฎํฅ,ํก), with syntactic form ํํํ (ํด(ยฎํฅ,ํก),ํ ) โกฮ ํด (ยฎํฅ,ํ ). (2) Here,ฮ ํด (ยฎํฅ,ํ )is a first order formula with free variables among ยฎํฅ,ํ . Moreover, the formula on the right hand side of (2) is uniform in s 1 . The following sentences states the condition under which the 1 A formulaํ(ํ )is uniform in a situation termํ ifํ is the only situation term that all the fluents occurring in ํ(ํ ) mention as their last argument. primitive actions listed above may be performed: ํํํ (ํขํํํํํ(ํ,ํก),ํ ) โก ํํํ(ํ)โงํํก(ํ,ํ )โงํํํํํํ(ํ,ํ ), (3) ํํํ (ํํํํ(ํ,ํก),ํ ) โก ํํํํ(ํ,ํ )โงํํก(ํ,ํ )โงํํํ(ํ), (4) ํํํ (ํํํฃํํํ(ํ,ํก),ํ ) โก ํกํํขํ, (5) ํํํ (ํํํํ ํตํขํกํํ(ํ,ํ,ํก),ํ ) โก ํํก(ํ,ํ )โงํํํ(ํ)โงํ= ํธ, (6) ํํํ (ํํํกํํํฆ(ํ,ํก),ํ ) โก ํกํํขํ. (7) Successor State Axioms. There is one for each(ํ+1)-ary rela- tional fluent ํน , with the following syntactic form: ํน(ยฎํฅ,ํํ(ํ,ํ )) โกฮฆ ํน (ยฎํฅ,ํ,ํ ). (8) In addition, there is one such axiom for each(ํ+1)-ary functional fluent ํ , with the following syntactic form: ํ(ยฎํฅ,ํํ(ํ,ํ ))=ํฆ โกฮฆ ํ (ยฎํฅ,ํฆ,ํ,ํ ). (9) The formulas on the right hand sides of (8) and (9) are uniform in s, andฮฆ ํน (ยฎํฅ,ํ,ํ )as well asฮฆ ํ (ยฎํฅ,ํฆ,ํ,ํ )are formulas with free vari- ables amongยฎํฅ,ํ,ํ andยฎํฅ,ํฆ,ํ,ํ , respectively. The formulaฮฆ ํน (ยฎํฅ,ํ,ํ ) specifies how actions of the domain impact the truth value of a relational fluent ํน and has the following canonical form [27]: ํพ + ํน (ยฎํฅ,ํ,ํ )โจ ํน(ยฎํฅ,ํ )โงยฌํพ โ ํน (ยฎํฅ,ํ,ํ ),(10) whereํพ + ํน (ยฎํฅ,ํ,ํ )(ํพ โ ํน (ยฎํฅ,ํ,ํ )) denotes a first order formula specify- ing the conditions that make a fluentํนtrue (false) in the situation following the execution ofํ. The formulaฮฆ ํ (ยฎํฅ,ํฆ,ํ,ํ )specifies how actions of the domain impact functional fluents; its canonical form is similar to the one forฮฆ ํน (ยฎํฅ,ํ,ํ ). Successor state axioms for the fluents of the door opening domain are as follows: ํํํํ(ํ,ํํ(ํ,ํ )) โก (โํก,ํ)ํ=ํขํํํํํ(ํ,ํก)โง (ํ= ํธโง ํํํํ ํตํขํกํํ(ํ,ํ,ํก))โจ ํํํํ(ํ,ํ )โงํโ ํํํํ(ํ,ํก), (11) ํํํํํํ(ํ,ํํ(ํ,ํ )) โก (โํก)ํ=ํํํํ(ํ,ํก)โจ(ํํํํํํ(ํ,ํ )โง ยฌ(โํก โฒ ,ํ)(ํ= ํธโงํ= ํํํํ ํตํขํกํํ(ํ,ํ,ํก โฒ ))), (12) ํํก(ํ,ํํ(ํ,ํ )) โก (โํก)ํ=ํํํฃํํํ(ํ,ํก)โจ ํํก(ํ,ํ )โงยฌ(โํ โฒ ,ํก โฒ )ํํํฃํํํ(ํ โฒ ,ํก โฒ ), (13) ํํํกํํํํํํํํํํํํ(ํํ(ํ,ํ ))=ํ โก (โํก)(ํํํํํํํ(ํ)โง ํ= ํํํกํํํฆ(ํ,ํก))โจํํํกํํํํํํํํํํํํ(ํ ). (14) 3 Ideality and possible worlds approaches While ideality is a normative ordering over those worlds that as- sesses how well each one satisfies obligations or norms. As a seman- tic tool, possible worlds explain the various ways the world could be, indicating alternative situations or states of affairs. In possible worlds, every world corresponds to a full description of a situation, including what is true, what happened, what obligations hold, etc [10][26]. Some research have been done to introduce the obligation con- cept of the Standard Deontic Logic (SDL) into the Situation Calculus [5] and [6]. Authors ranked deontic alternatives in terms of their levels of ideality; they subsequently define the obligatory sentences as those that are true in all alternative situations with maximal ideality; and finally, they give a successor state axiom for the fluent LAWโ26 Legal Agent Workshop, June 2026, Singapore, SingaporeKalonji Kalala et al. O. By contrast, our work simplifies the formalization by removing any use of situation idealities and by solely embedding the possible world semantics for SDL from [14] in the Situation Calculus. We use the possible worlds approach the same way Governatori in [9] [8] used it to incorporate the possible worlds, typically to give a sequence semantics for norms and obligations. We use the intuition of using possible worlds semantics behind the sequence semantics for norms and obligation, and extend it to the situation Calculus to reason about the obligations. 4 Obligations in the Situation Calculus 4.1A Deontic Fluent for Expressing Obligations To embed the possible worlds typically used to give a semantics to the Standard Deontic Logic (SDL) from [33] into the Situation Calculus, we need a binary deontic accessibility relation over situa- tions, where some situationํ โฒ is seen as being accessible from some other situationํ such that, as far as the agent located in situationํ is concerned, anything obligatory to that agent inํ must be true in situationํ โฒ . In this way, something being obliged in situationํ means that something is true in all situationsํ โฒ which are deontic accessible situations from ํ . Like in [5], we treat obligation as a fluent by introducing a binary relationํ(ํ โฒ ,ํ ), to be read as โํ โฒ is deontically accessible fromํ ". We can now define Oblg as a necessity operator over theํ-accessibility relation: (โํ โฒ ).O(ํ โฒ ,ํ ) โ ํ [ ํ โฒ ] ,(15) whereํ[ํ โฒ ]is the formulaํwith situation arguments added recur- sively to fluents that occur inํ. The following expresses that it is obligatory to have the ํํํ locked: (โํ โฒ ).ํ(ํ โฒ ,ํ ) โ ํํํํํํ(ํ,ํ โฒ ). (16) The notationOblg(ํ,ํ )says that the formulaํis obligatory in situation ํ : Oblg(ํ,ํ ) def = (โํ โฒ ).O(ํ โฒ ,ํ ) โ ํ [ ํ โฒ ] .(17) The formulaํused in the abbreviation (17) represents a formula obtained from a Situation Calculus formula by recursively sup- pressing its situation arguments. Conversely,ํ[ํ ]represents a Situation Calculus formula obtained by recursively restoring its suppressed situation arguments. This abbreviation (17) as well as the formula (15) are based on the semantic condition(ํถ.ํ + )given in [13] as Kripke semantics for the obligation modality. For example, Oblg ํํํํํํ(ํ),ํ expands as follows: Oblg(ํํํํํํ(ํ),ํ ) def =(โํ โฒ ).ํ(ํ โฒ ,ํ ) โ ํํํํํํ(ํ,ํ โฒ ). (18) Finally, we introduce an abbreviation to capture the fact that it is obligatory that ํก denotes ํฅ in all situations: Oref(ํก,ํ ) def = (โํฅ)(โํ โฒ ).ํ(ํ โฒ ,ํ ) โ ํก[ํ โฒ ]= ํฅ,(19) which can be equivalently expressed as follows: Oref(ํก,ํ ) def = (โํฅ)Oblg(ํก= ํฅ,ํ ). 4.2 Obligation-Producing Actions Among actions of the domain, some do affect what is happening in the world and obligation-producing actions do affect an agentโs state of obligations 2 . We call the later , by reference to knowledge- producing actions introduced by Scherl and Levesque in [31]. At the atomic level, obligation-producing actions are of two kinds: those actions whose effect is to make some (atomic) formula oblig- atory, and those whose effects is to make the denotation of some term obligatory. As an example of the first kind, the ground ac- tionํขํํํํํ(ํท,10)executed by the agent in situationํ 0 makes the ground atomic formulaํํํํํํ(ํท,ํํ(ํขํํํํํ(ํท,10),ํ 0 ))oblig- atory. In other words, the following sentence is made true by the execution of the actionํขํํํํํ(ํท, 10): Oblg(ํํํํํํ(ํท),ํํ(ํขํํํํํ(ํท, 10),ํ 0 )). (20) In our example,ํขํํํํํ(ํ,ํก)is an obligation-producing action that creates the obligation for the agent to subsequently get the door locked. The obligation produced is expressed by the ground sen- tence (20); that is, by executing the actionํขํํํํํ(ํท,10)in situation ํ 0 , the agent has the obligation to make sure that in some situation ํfollowing the situationํํ(ํขํํํํํ(ํท,10),ํ 0 ),ํํํํํํ(ํท,ํ)is true by virtue of an action executed by the agent to makeํํํํํํ(ํท,ํ) true. In general, we assume that there is a provision of (finitely many) obligation-producing actionsํ ํน ํ (ยฎํฅ ํ ,ํ ) whereํ=1. . .ํ, and that for each one of them, there is a fluentํน ํ (ยฎํฅ ํ ,ํ ),ํ=1. . .ํ, of the domain that is made obligatory in situationํํ(ํ ํน ํ (ยฎํฅ ํ ),ํ ) upon the execution ofํ ํน ํ (ยฎํฅ ํ ,ํ ) in situationํ . It is important to notice the difference between knowledge-producing actions of Scherl and Levesque and obligation-producing actions that are introduced here. The execution of a knowledge-producing actionํ= ํด ํ (ยฎํฅ ํ ) which is associated with a fluentํน ํ (ยฎํฅ ํ ,ํ )leads to the knowledge of the truth value ofํน ํ (ยฎํฅ ํ ,ํ ), whatever that truth value is, whereas the execution (in situationํ) of an obligation-producing action ํ= ํด ํ (ยฎํฅ ํ )which is associated with a fluentํน ํ (ยฎํฅ ํ ,ํ )leads to the obligation of the positive truth value of ํน ํ (ยฎํฅ ํ ,ํํ(ํด ํ (ยฎํฅ ํ ),ํ)). For the second kind of obligation-producing actions, we assume that there is a provision of (finitely many) such actionsํ ํ ํ (ยฎํฅ ํ ) whereํ=1. . .ํ, and that for each one of them, there is a functional fluentํ ํ (ยฎํฅ ํ ),ํ=1. . .ํ, of the domain whose denotation is made obligatory to the agent. As an example of the second kind of obligation-producing ac- tions, we haveํํํํ(ํ,ํก). By executing the ground actionํํํํ(ํท,20) in the ground situationํ, the agent makes the following ground atomic formula true: (โํ)Oblg(ํํํกํํํํํํํํํํํํ(ํํ(ํํํํ(ํท, 20),ํ))=ํ).(21) Thus,ํํํํ(ํ,ํก)is an obligation-producing action that creates the obligation for the agent to get the manager notified. This obligation is expressed by the sentence (21). 2 Some may do both, as we shall see later. Obligation-Producing Actions in Situation CalculusLAWโ26 Legal Agent Workshop, June 2026, Singapore, Singapore 5 Solving the Frame Problem 5.1 Successor State Axiom for the Fluent ํ Solving the frame problem consists in giving successor state axioms for all fluents of the domain as done in [29]. So, we need a successor state axiom for the fluent ํ . Suppose the agent executes the actionํํํฃํํํ(ํท,20)inํ 0 where no obligation holds andํํํํํํ(ํท,ํ 0 )is true. Then, the sentence ํํก(ํท,ํํ(ํํํฃํํํ(ํท,20),ํ 0 ))holds, and no new obligation is intro- duced. Now, ifํขํํํํํ(ํท,30)is executed at time t = 30, the sen- tence ํํํํ(ํท,ํํ(ํขํํํํํ(ํท, 30),ํํ(ํํํฃํํํ(ํท, 20),ํ 0 ,ํ 0 ))) holds and the agent has the obligation of subsequently locking the door. Finally, the execution ofํํํํ(ํท,40)will stop the obligation for the agent to get the door locked. The above consideration leads to three sorts of actions. The first sort is made of a provision of ordinary actions that do not produce any obligation with respect to the agent and do not release any existing obligations. The second sort is made of ordinary actions that do not produce any obligation, but they stop existing obligation. Finally, the third sort is made of obligation-producing actions. To start, suppose that a deontic agent is located in a situation ํ . We can imagine several infinitely many situationsํ โฒ 1 ,ํ โฒ 2 ,ํ โฒ 3 , . . ., which are deontic alternatives toํ . Furthermore, suppose that the deontic agent performs some actionํinํ and therefore lands in the successor situationํํ(ํ,ํ ). We now wonder what are the deontic alternatives toํํ(ํ,ํ ), and how these alternatives are related to the situationsํ โฒ 1 ,ํ โฒ 2 ,ํ โฒ 3 , . . .. We must come up with successor state axioms for the three sorts of actions identified above by spelling out how an action ํ affects the fluent ํ . 5.1.1 Non Obligation-Producing Actions. Consider the case of non obligation-producing actions that only change the truth value of some fluent, without introducing new obligations nor stopping existing ones. In this case, the deontic alternativesํ โฒ 1 ,ํ โฒ 2 ,ํ โฒ 3 , . . .to ํํ(ํ,ํ )will be related to the deontic alternativesํ โ 1 ,ํ โ 2 ,ํ โ 3 , . . .toํ as if the actionํwould have been performed in the later situations, such that ํ โ ํ =ํํ(ํ,ํ โฒ ํ ), for ํ= 1, 2, 3, . . .. In summary we have 3 : ํ(ํ โฒ ,ํํ(ํ,ํ )) โก (โํ โ ).ํ(ํ โ ,ํ )โงํ โฒ =ํํ(ํ,ํ โ ).(22) This means that these ordinary actions do not introduce new obli- gations to those that are already in place in the situationํ and in all the situations that areํ-accessible to the situationํ : the situa- tionํ โฒ which isํ-accessible toํํ(ํ,ํ )will be a mere reflection of the situationํ โ which isํ-accessible toํ . Figure 1 illustrates the sentence (22). In the door opening example, the actionํํํฃํํํ(ํ,ํก)is of this sort. For this action, we have the following characterization forํ: ํ(ํ โฒ ,ํํ(ํํํฃํํํ(ํ,ํก),ํ )) โก (โํ โ ).ํ(ํ โ ,ํ )โงํ โฒ =ํํ(ํํํฃํํํ(ํ,ํก),ํ โ ). (23) 3 We assume that the situations involved in successor state axioms are executable in the following sense: ํํฅํํ(ํ )= ํํ (โํ,ํ โฒ ).ํํ(ํ,ํ โฒ ) โ ํ โ ํํํ (ํ,ํ โฒ )โงํ ํกํํํก(ํ โฒ ) โค ํกํํํ(ํ). Here, we assume axioms that specify the occurrence timeํกํํํ(ํ)of actions and the start timeํ ํกํํํก(ํ ) of situations. Figure 1: Situations that areํ-related toํํ(ํ,ํ )whenํis not an obligation-producing action Figure 2: Situations that areํ-related toํํ(ํ,ํ )whenํis an Obligation-Releasing action In essence, this characterization of the fluentํdoes not differ from the one for non-knowledge-producing actions of Scherl and Levesque. 5.1.2 Obligation-Releasing Actions. We now turn to the case of non obligation-producing actions (which we call Obligation-Releasing Actions) that change the truth value of those fluents of the domain which are associated with obligation-producing actions, and, by doing so, they stop some existing obligations. In our door opening scenario,ํํํกํํํฆ(ํ,ํก)is such an action. Consider the reasoning we started with at the beginning of the present subsection. Suppose the agent is in the following situation with specified timeํ= ํํ(ํํํํ(ํท,40),ํํ(ํขํํํํํ(ํท,30),ํํ(ํํํฃํํํ(ํท,20),ํ 0 ))), where (โํ)Oblg(ํํํกํํํํํํํํํํํํ= ํ,ํ )becomes true. At this point the agent must ensure to notify some managerํin some subse- quent situation and at some time, e.g., 50, that the door is closed. This happens when the agent executes the actionํํํกํํํฆ(ํ,50). So, we reach the situationํํ(ํํํกํํํฆ(ํ),ํ), in that situation the obligation formula :(โํ)Oblg(ํํํกํํํํํํํํํํํํ=ํ,ํ )ceases to be true. LAWโ26 Legal Agent Workshop, June 2026, Singapore, SingaporeKalonji Kalala et al. For any actionํ, the termination of the obligation ofํน ํ (ยฎํฅ ํ )for the agent in situationํํ(ํ,ํ )happens whenํน ํ (ยฎํฅ ํ ,ํํ(ํ,ํ ))holds, which in turn happens when the formulaฮฆ ํน ํ (ยฎํฅ ํ ,ํ,ํ )becomes true. This justifies that we must produce a successor state axiom for ํwhich must entailํsentences of the following form, one for each of theํfluentsํน ํ (ยฎํฅ ํ )that are associated with the obligation- producing actions ํ ํน ํ (ยฎํฅ ํ ), 1โค ํ โค ํ: (โํ โฒ )[ํ(ํ โฒ ,ํ ) โ ํน ํ (ยฎํฅ ํ ,ํ โฒ )]โง ฮฆ ํน ํ (ยฎํฅ ํ ,ํ,ํ ) โยฌ(โํ โ )[ํ(ํ โ ,ํํ(ํ,ํ )) โ ํน ํ (ยฎํฅ ํ ,ํ โ )]. (24) Figure 2 illustrates the sentence (24). The figure shows that the sit- uations that areํ-alternatives toํํ(ํ,ํ ), whereํis an obligation- releasing action associated withํน ํ andฮฆ ํน ํ (ยฎํฅ ํ ,ํ,ํ )is true, are the images ofํ-alternatives toํ under the performance ofํin which we select those images where ํน ํ is false. An argument similar to the case of obligation termination can be made for obligation persistence. Sentences (25) give the sufficient conditions for the obligationsโs persistence: (โํ โฒ )[ํ(ํ โฒ ,ํ ) โ ํน ํ (ยฎํฅ ํ ,ํ โฒ )]โง ยฌฮฆ ํน ํ (ยฎํฅ ํ ,ํ,ํ ) โ (โํ โ )[ํ(ํ โ ,ํํ(ํ,ํ )) โ ํน ํ (ยฎํฅ ํ ,ํ โ )]. (25) Again, one such sentence must be entailed by the successor state axiom forํfor each of theํfluentsํน ํ (ยฎํฅ ํ )that are associated with the obligation-producing actions ํ ํน ํ (ยฎํฅ ํ ), 1โค ํ โค ํ. 5.1.3 Obligation-Producing Actions. We specify how an obligation- producing actionํ ํน ํ (ยฎํฅ ํ ) that is associated with a fluentํน ํ (ยฎํฅ ํ ) affects the fluentํ. Recall that the actionํ ํน ํ (ยฎํฅ ํ ) , which is executed in a situationํ , is understood to make the positive truth value of ํน ํ (ยฎํฅ ํ )obligatory in the successor situationํํ(ํ ํน ํ (ยฎํฅ ํ ),ํ ) . Thus, in this case, we want thatOblg(ํน ํ (ยฎํฅ ํ ),ํํ(ํ ํน ํ (ยฎํฅ ํ ),ํ )) holds. This leads to the following characterization of the fluent ํ : ํ(ํ โฒ ,ํํ(ํ ํน ํ (ยฎํฅ ํ ),ํ )) โก (โํ โ ,ํ).ํ(ํ โ ,ํ )โงํ โฒ =ํํ(ํ(ยฎํฅ ํ ),ํ โ )โง ํน ํ (ยฎํฅ ํ ,ํํ(ํ,ํ โ )). (26) Using the successor state axiom (8) and the canonical form (10) of its right-hand side, we get the following: ํน ํ (ยฎํฅ ํ ,ํํ(ํ,ํ โ )) โกฮฆ ํน ํ (ยฎํฅ ํ ,ํ,ํ ), (27) which brings the sentence (26) to become: ํ(ํ โฒ ,ํํ(ํ ํน ํ (ยฎํฅ ํ ),ํ )) โก (โํ โ ,ํ โฒ ).ํ(ํ โ ,ํ )โงํ โฒ =ํํ(ํ โฒ (ยฎํฅ ํ ),ํ โ )โงฮฆ ํน ํ (ยฎํฅ ํ ,ํ โฒ ,ํ ). (28) Sentence (28) tells us that the situations that are consideredํ- related toํํ(ํ ํน ํ (ยฎํฅ ํ ),ํ )are those obtained by performing some (non obligation-producing) actionํ โฒ in situationsํ-related toํ in whichฮฆ ํน ํ (ยฎํฅ ํ ,ํ โฒ ,ํ )evaluates toํกํํขํ. Referring to sentence (28), we obtain the following sentence for each obligation-producing action ํ ํน ํ (ยฎํฅ ํ ), 1โค ํ โค ํ: ํ=ํ ํน ํ (ยฎํฅ ํ ) โ [ํ(ํ โฒ ,ํํ(ํ(ยฎํฅ ํ ),ํ )) โก (โํ โ ,ํ โฒ ).ํ(ํ โ ,ํ )โงํ โฒ =ํํ(ํ โฒ (ยฎํฅ ํ ),ํ โ )โงฮฆ ํน ํ (ยฎํฅ ํ ,ํ โฒ ,ํ โ )]. (29) Notice that an obligation-producing actionํ ํน ํ executed inํ , is supposed to make theํน ํ obligatory inํํ(ํ ํน ํ ,ํ ). Henceforth, for any situationํ โ such thatยฌํน ํ (ํ โ )holds,ํ โ must not be considered as a doxatic alternative toํํ(ํ ํน ํ ,ํ ). Those situations whereํน ํ (ํ โ ) Figure 3: Situations that areํ-related toํํ(ํ,ํ )whenํis an obligation-producing action producing an obligation ํน ํ holds will be retained as the situations that areํ-accessible to ํํ(ํ ํน ํ ,ํ ) : they are exactly the images, under the performance of actionํ โฒ , of theํ-accessible situation toํ , where actionํ โฒ is the one free action variable mentioned inฮฆ ํน ํ (ยฎํฅ ํ ,ํ โฒ ,ํ โ ) . Figure 3 illustrates the sentence (29). Given the provision of (finitely many) obligation-producing ac- tionsํ ํน ํ (ยฎํฅ) whereํ=1. . .ํ, assume that they are associated with relational fluentsํน ํ (ยฎํฅ),ํ=1. . .ํ. Moreover, given a further provision of (finitely many) obligation-producing actionsํ ํ ํ (ยฎํฅ) whereํ=1. . .ํ, assume that they are associated functional fluents ํ ํ (ยฎํฅ),ํ=1. . .ํ. We are now in position to draw the final conclu- sion about the characterization of the fluentํ: the sentences (22), (24), (25), and (29) can be put together in the equivalent sentence (30) (that takes into account functional fluents) shown in Figure 4. Sentence (30) is our proposed successor state axiom forํ. The sentence (31) in Figure 5 is the successor state axiom forํin our running example. 5.2 General Successor State Axiom for ํ The successor state axiom forํaxiom (30) assumes that obligations are atomic fluents. We need to generalize this axiom by considering obligations that are general formulas. Assume that we have a provi- sion of obligation-producing actionsํ ํ ํ (ยฎํฅ ํ ) ,ํ=1. . .ํ, each asso- ciated with an arbitrary formulaํ ํ (ยฎํฅ ํ ),ํ=1. . .ํ. These formulas ํ ํ (ยฎํฅ)are the so-called "objective situation-suppressed sentences" ("Objective sentences" for short) of Reiter [27]: they are about the world and do not mention the abbreviationOblg. Furthermore assume, without loss of generality, thatํ ํ (ยฎํฅ ํ )is the conjunction ํบ 1 (ยฎํฅ 1 )โง . . .โงํบ ํ (ยฎํฅ ํ )of atomic formulasํบ ํ (ยฎํฅ ํ ),ํ=1. . .ํ. Also, assume thatโ ํ ํ (ยฎํฆ ํ ,ํ,ํ ) is the conjunctionฮฆ ํบ 1 (ยฎํฅ 1 ,ํ 1 ,ํ 1 )โงยทโง ฮฆ ํบ ํ (ยฎํฅ ํ ,ํ 1 ,ํ 1 ) of atomic formulasฮฆ ํบ ํ , ํ= 1. . .ํ . Here the formula ฮฆ ํบ ํ (ยฎํฅ ํ ,ํ ํ ,ํ ํ )represents the right-hand side of the successor state axiom for the fluentํบ ํ (ยฎํฅ ํ ). We can generalize the axiom (30) by using the general formulasํ ํ instead of atomic fluents: we omit this here for lack of space. Obligation-Producing Actions in Situation CalculusLAWโ26 Legal Agent Workshop, June 2026, Singapore, Singapore Figure 4: Successor state axiom for the fluent ํ ํ(ํ โฒ ,ํํ(ํ,ํ )) โก [(โํ โ ,ํ โฒ ).ํ(ํ โ ,ํ )โงํ โฒ =ํํ(ํ โฒ ,ํ โ )โง [[[ํโ ํ ํน 1 (ยฎํฆ 1 )โง . . .โงํโ ํ ํน ํ ( ยฎํฆ ํ )โง ํโ ํ ํ 1 (ยฎํง 1 )โง . . .โงํโ ํ ํ ํ (ยฎํง ํ )โงํ= ํ โฒ ]โง (โยฎํฅ 1 )[(ํน 1 (ยฎํฅ 1 ,ํ โ )โงฮฆ ํน 1 (ยฎํฅ 1 ,ํ,ํ ) โยฌํน 1 (ยฎํฅ 1 ,ํ โฒ )]โง . . .โง (โ ยฎํฅ ํ )[(ํน ํ ( ยฎํฅ ํ ,ํ โ )โงฮฆ ํน ํ ( ยฎํฅ ํ ,ํ,ํ ) โ ยฌํน ํ ( ยฎํฅ ํ ,ํ โฒ )]โง (โยฎํฅ 1 )[(ํน 1 (ยฎํฅ 1 ,ํ โ )โงยฌฮฆ ํน 1 (ยฎํฅ 1 ,ํ,ํ ) โ ํน 1 (ยฎํฅ 1 ,ํ โฒ )]โง . . .โง (โ ยฎํฅ ํ )[(ํน ํ ( ยฎํฅ ํ ,ํ โ )โงยฌฮฆ ํน ํ ( ยฎํฅ ํ ,ํ,ํ ) โ ํน ํ ( ยฎํฅ ํ ,ํ โฒ )]โง (โยฎํฅ 1 ,ํฆ 1 )[(ํ 1 (ยฎํฅ 1 ,ํ โ )=ํฆ 1 โง ฮฆ ํ 1 (ยฎํฅ 1 ,ํฆ 1 ,ํ,ํ ) โ ํ 1 (ยฎํฅ 1 ,ํ โฒ )โ ํฆ 1 ]โง . . .โง (โยฎํฅ ํ , ยฎํฆ ํ )[(ํ ํ (ยฎํฅ ํ ,ํ โ )= ยฎํฆ ํ โง ฮฆ ํ ํ (ยฎํฅ ํ , ยฎํฆ ํ ,ํ,ํ ) โ ํ ํ (ยฎํฅ ํ ,ํ โฒ )โ ยฎํฆ ํ ]โง (โยฎํฅ ํ , ยฎํฆ 1 )[(ํ 1 (ยฎํฅ 1 ,ํ โ )= ยฎํฆ 1 โง ยฌฮฆ ํ 1 (ยฎํฅ 1 , ยฎํฆ 1 ,ํ,ํ ) โ ํ 1 (ยฎํฅ 1 ,ํ โฒ )= ยฎํฆ 1 ]โง . . .โง (โํฅ ํ ,ํฆ ํ )[(ํ ํ (ยฎํฅ ํ ,ํ โ )= ยฎํฆ ํ โง ยฌฮฆ ํ ํ (ยฎํฅ ํ , ยฎํฆ ํ ,ํ,ํ ) โ ํ ํ (ยฎํฅ ํ ,ํ โฒ )= ยฎํฆ ํ ]]โจ [(โํฅ 1 )[ํ= ํ ํน 1 (ยฎํฅ 1 ) โฮฆ ํน 1 (ยฎํฅ 1 ,ํ โฒ ,ํ โ )]โง . . .โง (โํฅ ํ )[ํ= ํ ํน ํ ( ยฎํฅ ํ ) โฮฆ ํน ํ ( ยฎํฅ ํ ,ํ โฒ ,ํ โ )]โง (โยฎํฆ 1 , ยฎํฆ 1 )[ํ= ํ ํ 1 (ยฎํฅ 1 ) โฮฆ ํ 1 (ยฎํฅ 1 , ยฎํฆ 1 ,ํ โฒ ,ํ โ )]โง . . .โง (โํฅ ํ , ยฎํฆ ํ )[ํ= ํ ํ ํ (ยฎํฅ ํ ) โฮฆ ํ ํ (ยฎํฅ ํ , ยฎํฆ ํ ,ํ โฒ ,ํ โ )]]]]. (30) 5.3 Correctness The formalization is correct in the sense that, an obligation-producing action creates an obligation in the successor situation and if a fluent is obligatory in a given situation, it remains so, unless an action that causes the obligation to stop is executed. Theorem 5.1. (Correctness) For all actionsํผ, fluentsํน ํ , and situations ํ the following holds: (1) (Obligation Creation): Ifํผ= ํ ํน ํ (ยฎํฅ ํ ) , whereํ ํน ํ (ยฎํฅ ํ ) is the obligation-producing action associated withํน ํ , then the following Oblg(ํน ํ (ยฎํฅ ํ ),ํํ(ํผ,ํ )) holds. (2) (Obligation Stoppage): IfOblg(ํน ํ (ยฎํฅ ํ ),ํ )andฮฆ ํน ํ (ยฎํฅ ํ ,ํผ,ํ )hold, thenยฌOblg(ํน ํ (ยฎํฅ ํ ),ํํ(ํผ,ํ )) holds. (3) (Obligation Persistence): IfOblg(ํน ํ (ยฎํฅ ํ ),ํ )andยฌฮฆ ํน ํ (ยฎํฅ ํ ,ํผ,ํ ) hold, then Oblg(ํน ํ (ยฎํฅ ํ ),ํํ(ํผ,ํ )) holds. Proof. Proof: (1): For lack of space, we omit the proof. (2): Suppose that, for some ground object tuple ยฎ ํ ํ , some ground actionํด, and some ground situationํ,ฮฆ ํน ํ (ยฎํฅ ํ ,ํด,ํ)holds. Moreover, assume that we execute some ground actionํด( ยฎ ํ)inํ. Then, by the successor state axiom forํน,ํน( ยฎ ํ ํ )holds in the subsequent situationํํ(ํด( ยฎ ํ),ํ). Furthermore, by assumption we have that Oblg(ํน ํ ( ยฎ ํ ํ ),ํ)holds; hence, by the abbreviation (17), we get the Figure 5: Example of Successor state axiom for the fluent ํ ํ(ํ โฒ ,ํํ(ํ,ํ )) โก [(โํ โ ,ํ โฒ ).ํ(ํ โ ,ํ )โงํ โฒ =ํํ(ํ โฒ ,ํ โ )โง [[[ํโ ํขํํํํํ(ํ,ํก)โงํโ ํํํํ(ํ,ํก)โงํ= ํ โฒ ]โง (โํ)[(ํํํํํํ(ํ,ํ โ )โง((โํก)(ํ=ํํํํ(ํ,ํก)โจ ํํํํํํ(ํ,ํ )โงยฌ(โํ,ํก โฒ )ํ= ํํํํ ํตํขํกํํ(ํ,ํ,ํก โฒ ))] โ ยฌํํํํํํ(ํ,ํ โฒ )]โง (โํ)[(ํํํํํํ(ํ,ํ โ )โงยฌ((โํก)(ํ=ํํํํ(ํ,ํก)โจํํํํํํ(ํ,ํ )โง ยฌ(โํ,ํก โฒ )ํ= ํํํํ ํตํขํกํํ(ํ,ํ,ํก โฒ ))] โ ํํํํํํ(ํ,ํ โฒ )]โง (โํ)[(ํํํกํํํํํํํํํํํํ(ํ โ )=ํโง((โํก โฒ )(ํํํํํํํ(ํ,ํ )โง ํ= ํํํกํํํฆ(ํ,ํก โฒ ))โจํํํกํํํํํํํํํํํํ(ํ )โง ยฌ(โํ โฒ ,ํก โฒ )ํ= ํํํกํํํฆ(ํ โฒ ,ํก โฒ )) โ ํํํกํํํํํํํํํํํํ(ํ โฒ )โ ํ]โง (โํ)[(ํํํกํํํํํํํํํํํํ(ํ โ )=ํโงยฌ((โํก โฒ )(ํํํํํํํ(ํ,ํ )โง ํ= ํํํกํํํฆ(ํ,ํก โฒ ))โจํํํกํํํํํํํํํํํํ(ํ )โง ยฌ(โํ โฒ ,ํก โฒ )ํ= ํํํกํํํฆ(ํ โฒ ,ํก โฒ )) โ ํํํกํํํํํํํํํํํํ(ํ โฒ )=ํ]]โจ [(โํ,ํก)[ํ=ํขํํํํํ(ํ,ํก) โ ((โํก โฒ )ํ โฒ =ํํํํ(ํ,ํก โฒ )โจ ํํํํํํ(ํ,ํ โ )โงํ โฒ โ ํํํํ ํตํขํกํํ(ํ,ํก โฒ ))]โง [(โํ,ํก)[ํ=ํํํํ(ํ,ํก) โ ((โํ,ํก โฒ )(ํํํํํํํ(ํ,ํ โ )โง ํ โฒ = ํํํกํํํฆ(ํ,ํก โฒ ))โจํํํกํํํํํํํํํํํํ(ํ โ )โง ยฌ(โํ โฒ ,ํก โฒ )ํ โฒ = ํํํกํํํฆ(ํ โฒ ,ํก โฒ ))]]]]. (31) (32) following: (โํ โ )O(ํ โ ,ํ)) โ ํน ํ ( ยฎ ํ,ํ โ ).(33) We must now show thatํน ํ ( ยฎ ํ,ํ)ceases to be obligatory inํํ(ํด( ยฎ ํ ํ ),ํ; that is, we must show thatยฌOblg(ํน ํ ( ยฎ ํ ํ ),ํํ(ํด( ยฎ ํ ํ ),ํ))holds. To do so, suppose that we have some ground situationํ โฒ such that ํ(ํ โฒ ,ํํ(ํด( ยฎ ํ),ํ)). Then, by Axiom (30) and by the fact thatํดis not an obligation-producing action, the following sentence holds (after appropriate skolemization and simplifications): ํ(ํ โ ,ํ)โง ํ โฒ =ํํ(ํด,ํ โ )โง (โํฅ ํ )[(ํน ํ (ยฎํฅ ํ ,ํ โ )โงฮฆ ํน ํ (ยฎํฅ ํ ,ํด,ํ) โ ยฌํน ํ (ยฎํฅ ํ ,ํ โฒ )]. (34) By the sentence (33) and the assumptionฮฆ ํน ํ ( ยฎ ํ ํ ,ํด,ํ), the above sentence (34) yields the following: ํ(ํ โ ,ํ)โง ํ โฒ =ํํ(ํด,ํ โ )โงยฌํน ํ ( ยฎ ํ ํ ,ํ โฒ )]. (35) Since the sentence (35) holds for any fixed situationํandํ โ , we conclude thatยฌOblg(ํน ํ (ยฎํฅ ํ ),ํํ(ํผ,ํ )) holds. (3): The arguments of the proof are similar to the proof of obligation stoppage. We omit the proof.โก LAWโ26 Legal Agent Workshop, June 2026, Singapore, SingaporeKalonji Kalala et al. 6 Characterization of ํ in the Initial Situation Characterizing the fluentํin the initial situation is important, since, as it stands, the definition of obligation given in (17) does not differentiate the obligation modality from knowledge. Such a differ- entiation comes only in the form of appropriate properties which are unique to the deontic accessibility relationship. The space of situations is constrained by foundational axioms, which impose a structuring of that space in the form of a tree rooted in the initial sit- uationํ 0 [29]. To accommodate the introduction of knowledge, this ํ 0 -rooted tree semantics of the space of situations has been modi- fied in [31] with the introduction of the predicateํผํํํก(ํ )to capture initial situations for knowledge; and the specification given for this predicate still holds for obligations. The next abbreviation (36) and two axioms adapt Reiterโs version of the predicateํผํํํก(ํ )[27] to obligations: ํผํํํก(ํ ) def = ยฌ(โํ,ํ โฒ )ํ =ํํ(ํ,ํ โฒ ),(36) ํ(ํ ,ํ โฒ ) โ (ํผํํํก(ํ ) โก ํผํํํก(ํ โฒ )),(37) (โํ).(โํ )(ํผํํํก(ํ ) โ ํ(ํ ))โง(โํ,ํ )(ํ(ํ ) โ ํ(ํํ(ํ,ํ ))) โ (โํ )ํ(ํ ). (38) For deontic logic, the following restrictions are imposed to the predicate ํผํํํก(ํ ) to obtain different variants of SDL: Secondary Reflexivity: (โํ ,ํ โฒ ).ํผํํํก(ํ )โง ํผํํํก(ํ โฒ ) โ (ํ(ํ โฒ ,ํ ) โ ํ(ํ โฒ ,ํ โฒ )). (39) Seriality: (โํ ).ํผํํํก(ํ ) โ ((โํ โฒ ).ํผํํํก(ํ โฒ )โงํ(ํ โฒ ,ํ )).(40) Secondary Seriality: (โํ ).ํผํํํก(ํ )โ((โํ โฒ ).ํผํํํก(ํ โฒ )โงํ(ํ โฒ ,ํ )โงํ(ํ โฒ ,ํ โฒ )). (41) The properties above are used as restrictions to model various deontic logic systems. For example, von Wrightโs SDL is obtained by using Secondary Reflexivity and Seriality. Theorem 6.1. (Restriction Theorem) Suppose that the prop- erties of secondary reflexivity, secondary seriality, and seriality for theํrelation hold in all situationsํ such thatํผํํํก(ํ ). Then these properties also hold for the ํ relation in all executable situations. Proof. We use the induction principle for the situation calculus [25] as given in its weaker form in formula (38). So we must show that the properties (39), (40), and (41) hold in the initial situations, and that, if they hold in situationํ , then they also hold in executable situationsํํ(ํ,ํ ). Assume that they hold in initial situations. Thus, we only need to show that whenever they hold inํ , then they also hold in ํํ(ํ,ํ ). Secondary Reflexivity: Suppose that(โํ ,ํ โฒ ).ํ(ํ โฒ ,ํ ) โ ํ(ํ โฒ ,ํ โฒ ) holds forํ . We must prove that(โํ ,ํ โฒ ).ํ(ํ โฒ ,ํํ(ํ,ํ )) โ ํ(ํ โฒ ,ํ โฒ ) holds for everyํsuch asํํ(ํ,ํ )is executable. For the sentence (โํ ,ํ โฒ ).ํ(ํ โฒ ,ํํ(ํ,ํ )) โ ํ(ํ โฒ ,ํ โฒ )to be false there should be some ํ and someํ, such thatํ(ํ โฒ ,ํํ(ํ,ํ ))is true, butํ(ํ โฒ ,ํ โฒ )is false. According to the successor state axiom (30) for O, the formula ํ(ํ โฒ ,ํํ(ํ,ํ ))is true iffํ โฒ =ํํ(ํ,ํ โฒ )for someํ โฒ , andํ(ํ โฒ ,ํ )as well as further conditions on the right-hand side of the axiom (30) are true. By assumption, ifํ(ํ โฒ ,ํ )is true, thenํ(ํ โฒ ,ํ โฒ )must be true as well. Therefore(โํ ,ํ โฒ ).ํ(ํ โฒ ,ํํ(ํ,ํ )) โ ํ(ํ โฒ ,ํ โฒ )cannot be false. Seriality: Assume that(โํ )(โํ โฒ )ํ(ํ โฒ ,ํ )holds. We must show that (โํ )(โํ โฒ )ํ(ํ โฒ ,ํํ(ํ,ํ ))holds for everyํsuch asํํ(ํ,ํ )is exe- cutable. For(โํ )(โํ โฒ )ํ(ํ โฒ ,ํํ(ํ,ํ ))to be false, we will have the case where, for someํ , noํ โฒ is such thatํ(ํ โฒ ,ํํ(ํ,ํ ))is true. Notice that by the successor state axiom (30) for O, the unique alternative forํ(ํ โฒ ,ํํ(ํ,ํ ))to be true is forํ โฒ to be equal to ํํ(ํ,ํ โฒ )for someํ โฒ such thatํ(ํ โฒ ,ํ ), as well as further condi- tions on the right-hand side of the axiom (30) to hold. Then, ac- cording to the successor state axiom (30), and the assumption that ํ(ํ โฒ ,ํ )is true, it has to be the case thatํ(ํ โฒ ,ํํ(ํ,ํ )is true. There- fore(โํ โฒ )ํ(ํ โฒ ,ํ ) โ (โํ โฒ )ํ(ํ โฒ ,ํํ(ํ,ํ )), which contradicts our assumption. Secondary Seriality: Suppose that(โํ )(โํ โฒ )(ํ(ํ โฒ ,ํ )โงํ(ํ โฒ ,ํ โฒ )) is true for allํ . We must prove that(โํ )(โํ โฒ )(ํ(ํ โฒ ,ํํ(ํ,ํ )) โง ํ(ํ โฒ ,ํ โฒ )) holds for every a such asํํ(ํ,ํ )is executable. The rest of the proof goes by contradiction. We leave details out.โก 7 Reasoning About Obligations 7.1 Regression Regression is a type of proof theory that uses backward reasoning. Regression is a mechanism for transposing reasoning about the truth value of formulas in successor situations to reasoning about modified formulas in the initial situation. In the Situation Calculus, regression is the most crucial theorem- proving tool. In the type of regression mechanism proposed by Re- iter in [30], the reasoning about future situations is simply brought to the reasoning about the initial situationํ 0 [24]. The outcome of the regression is a formula in ordinary modal logic, meaning that it has no action terms and only has the situationโs term ํ 0 . In a regressable sentences, each situation term is rooted atํ 0 , so one can count the number of actions involved by examining the term. Reiterโs regression operator for reasoning about actions back to the initial situation is a reasoning mechanism for this setting as well. 7.2 Regressing Obligation Formulas We start by defining a formulaํof the Situation Calculus to be regressable iff it mentions only situation terms that are rooted inํ 0 , does not quantify over situations, and does not mention the predicate symbolโ, nor equality atoms over situation terms. Suppose we have a regressable formulaํwhere all situation terms have been suppressed. Then the one-step regression ofํthrough the actionํผ, denotedํ 1 (ํ,ํผ), is the following manipulation [27]: first take the formulaํand restore the situation argumentํํ(ํผ,ํ) to all fluents mentioned inํ, for someํ; then, regress the resulting formula; finally suppress all situations from the resulting regressed formula. The following Definition 7.1 accommodates formulas that mention Oblg: Definition 7.1. (Regression Operator for Obligations) Sup- poseํis a situation-suppressed (regressable) formula of the Situ- ation Calculus, andDis a basic action theory. Moreover, assume, without loss of generality, thatํis the conjunctionํบ 1 (ยฎํฅ 1 )โง . . .โง Obligation-Producing Actions in Situation CalculusLAWโ26 Legal Agent Workshop, June 2026, Singapore, Singapore ํบ ํ (ยฎํฅ ํ )of atomic formulasํบ ํ (ยฎํฅ ํ ),ํ=1. . .ํ, and thatโ ํ is the conjunctionฮฆ ํบ 1 โงยทโงฮฆ ํบ ํ of atomic formulasฮฆ ํบ ํ ,ํ=1. . .ํ. Here the formulaฮฆ ํบ ํ represents the right-hand side of the successor state axiom for the fluentํบ ํ (ยฎํฅ ํ ). Then, in addition to the regression steps described in [27] for regressable formulas, the following steps ac- commodate expressions of the formOblg(ํ,ํํ(ํผ,ํ)), whereํผis any of actions mentioned in Section 5.1: (i) An obligation in ํ 0 stops the regression process: R[Oblg(ํ,ํ 0 )]= Oblg(ํ,ํ 0 ). (i) Ifํผis a non obligation-producing action that is a non obligation-releasing one, then R[Oblg(ํ,ํํ(ํผ,ํ))]=R[ยฌโ ํ โง Oblg(ํ 1 (ํ,ํผ),ํ)]. (i) Ifํผis a non obligation-producing action which is an obligation-releasing one, then R[ยฌOblg(ํ,ํํ(ํผ,ํ))]=R[โ ํ โง Oblg(ํ 1 (ํ,ํผ),ํ)]. (iv) Ifํผis not an obligation-producing action which is neither an obligation-releasing one, nor a non obligation-releasing one, then R[Oblg(ํ,ํํ(ํผ,ํ))]=R[Oblg(ํ 1 (ํ,ํผ),ํ)]. (v) Ifํผ= ํด ํ ( ยฎ ํก)is an obligation-producing action that brings about the obligation of the formulaํfor some term ยฎ ํก, then R[Oblg(ํ,ํํ(ํผ,ํ))]=R[(โํผ โฒ )Oblg(ํ( ยฎ ํก) โ ํ 1 (ํ,ํผ โฒ ),ํ)]. (vi)Ifํผ= ํด( ยฎ ํก)is an obligation-producing action that requires the referent of a term ํก to be some individualํฆ, then R[Oblg(ํ,ํํ(ํผ,ํ))]=R[(โํฆ,ํผ โฒ )Oblg(ํก=ํฆ โ ํ 1 (ํ,ํผ โฒ ),ํ)]. In the sequel, the notationR โ [ํ]is used to denote a repeated application of the regression operator on the formulaํuntil fur- ther applications leaveํunchanged. We need to extend the basic action theories from [20] with new classes of axioms and revisit and/or extend some basic sentences of basic action theories for knowledge from [28]. The extensions essentially take into account the inclusion ofOblgandOrefin the action precondition axioms and axioms aboutํ 0 , and the inclusion of the successor state axiom forํ. With basic action theories for obligations in hand, we now have: Theorem 7.2. (The Regression Theorem with Obligations) Suppose thatDis a basic action theory for obligations, andํis a regressable sentence. LetD ํ 0 andD ํขํํ be the axioms describing the initial situation and unique name axioms, respectively. Moreover, suppose thatO ํผํํํก consists of the properties of secondary refexivity, and secondary seriality. Then D |=ํ iff D ํ 0 โชD ํขํํ โชO ํผํํํก |=R โ [ํ]. Proof.Outline. The proof extends the one for the basic regres- sion theorem given in [31] by handling the regression steps related to the obligation. Each one of the steps (i)-(vi) of the extended re- gression operator is justified by a proposition whereby the sentence mentioned on the left-hand and right-hand sides of the equality sign are shown to be logically equivalent.That is, each step of the regression preserves logical equivalence. the whole process termi- nates in ํ 0 after a finite number of steps. Case(i): The proof of the regression rule expressed by the the fol- lowingR[Oblg(ํ,ํ 0 )]= Oblg(ํ,ํ 0 )is immediate, since for a situation suppressed expressionํ with free variables ยฎํฅ , we have: D |=(โยฎํฅ).Oblg(ํ(ยฎํฅ),ํ 0 ) โก Oblg(ํ(ยฎํฅ),ํ 0 ). Case(i): Here the regression rule is justified by the following: supposeํis a situation suppressed expression with free variables ยฎํฅ, andํด(ยฎํฆ)is a non obligation-producing action that is a non obligation-releasing one; then D |=(โยฎํฅ,ยฎํฆ,ยฎํ ) Oblg ( ํ(ยฎํฅ), do(ํด(ยฎํฆ),ํ ) ) โก ยฌฮฆ ํบ 1 โงยทโงยฌฮฆ ํบ ํ โง Oblg ํ 1 (ํ(ยฎํฅ),ํด(ยฎํฆ)),ํ . Case(i): This regression rule is justified by the following: suppose ํis a situation suppressed expression with free variablesยฎํฅ, and ํด(ยฎํฆ)is a non obligation-producing action that is an obligation- releasing one; then D |=(โยฎํฅ,ยฎํฆ,ยฎํ ) Oblg(ํ(ยฎํฅ), do(ํด(ยฎํฆ),ํ )) โก ยฌโ ํ (ยฎํฅ)โง Oblg(ํ 1 (ํ(ยฎํฅ),ํด(ยฎํฆ)),ํ ). Case(iv): Supposeํis a situation suppressed expression with free variablesยฎํฅ, andํด(ยฎํฆ)is a non obligation-producing action that is neither an obligation-releasing one, nor a non obligation- releasing one ; then D |=(โยฎํฅ,ยฎํฆ,ํ ) Oblg(ํ(ยฎํฅ), do(ํด(ยฎํฆ),ํ )) โก (โํด โฒ ) Oblg(ํ(ยฎํฆ) โ ํ 1 (ํ(ยฎํฅ),ํด โฒ ), ํ ). Case(vi): Supposeํis a situation suppressed expression with free variablesยฎํฅ, andํด ํก (ํฆ)is an obligation-producing action that requires the referent of some term ํก to be an individualํฆ ; then D |=(โยฎํฅ,ํฆ,ํ ) Oblg(ํ(ยฎํฅ), do(ํด ํก (ํฆ),ํ )) โก (โํก,ํด โฒ ) Oblg(ํก=ํฆ) โ Oblg(ํ 1 (ํ(ยฎํฅ),ํด โฒ ),ํ ) . โก Theorem 7.2 states that in order to evaluate a sentenceํagainst a basic action theoryD, it is necessary and sufficient to evaluate R[ํ]in the initial theoryD ํ 0 augmented with unique name ax- ioms and properties of the relation ํ . 7.3 Example Suppose that the axiomatization of the initial situation includes ํํํ(ํท,ํ 0 ),ํํํํํํ(ํท,ํ 0 ), andํํก(ํท,ํ 0 ). Assume we regress the sentence 42. Oblg(ํํํํํํ(ํท),ํํ(ํํํํ ํตํขํกํํ(ํท, 20), ํํ(ํขํํํํํ(ํท, 10),ํ 0 ))))). (42) By the Step iv of Definition 7.1 on the sentence (42) we obtain: R[Oblg(ํ 1 (ํํํํํํ(ํท),ํํํํ ํตํขํกํํ(ํท, 20)), ํํ(ํขํํํํํ(ํท, 10),ํ 0 ))], (43) which, by the one-step reduction, expands to R[Oblg(ํํํํํํ(ํท),ํํ(ํขํํํํํ(ํท, 10),ํ 0 ))]. (44) Furthermore, recall thatํํํํํํ(ํ,ํ )is the formula that is associ- ated with the obligation-producing actionํขํํํํํ ํํํํํํ (ํ,ํ ); thus LAWโ26 Legal Agent Workshop, June 2026, Singapore, SingaporeKalonji Kalala et al. performing Step v of Definition 7.1 on the sentence (44) yields the sentence (45). R[(โํ โฒ ).Oblg(ํํํํํํ(ํท) โ ((โํก).ํ โฒ =ํํํํ(ํท,ํก)โจ ํํํํํํ(ํท)โงํ โฒ โ ํํํํ ํตํขํกํํ(ํท,ํก)),ํ 0 )]. (45) 8 Related Work Our obligation-producing actions in the Situation Calculus are similar to and a substantial modification of those that were first introduced in [5] and in [6], where the deontic accessibility rela- tionshipํwas introduced. In [5] and [6], authors ranked deontic alternatives in terms of their levels of ideality; they subsequently de- fine the obligatory sentences as those that are true in all alternative situations with maximal ideality; and, finally, they give a successor state axiom for the fluentํ. By contrast, our work simplifies the formalization by removing any use of situation idealities and by solely embedding the possible world semantics for SDL from [13] in the Situation Calculus. Furthermore, we expand Reiterโs regression to reason about obligation-producing actions. Another approach for incorporating deontic notions into the Situation Calculus is presented by Classen and Delgrande in [2]. In [2], deontic asser- tions and modalities are expressed as constraints that subsequently compiled into a Situation Calculus action theory which are used to reason about obligations. We differ from this approach by express- ing obligations directly in the Situation Calculus so that there is no need of an extra compilation step. Event Calculus described in [15] may also be used for specifying obligations (See [3], and [11]. The Situation Calculus, however, enjoys the key advantage of the existence of GOLOG (See in [19]), a Situation Calculus-based programming language for defining complex actions in terms of a set of primitive actions axiomatized in the Situation Calculus. 9 Conclusion and Future Work We have spelled out the formalization of obligations in the Situation Calculus around a deontic fluentํ, along with appropriate actions that change its truth value, as well as an appropriate successor state axiom for that deontic fluent. Furthermore, we stated the correctness of our approach as well as appropriate restrictions of the deontic fluent in the initial situations. Finally, we extended the regression operator, the main reasoning tool of Reiterโs framework, to obligations. One future work is the specification of smart legal contracts in the Situation Calculus. The plan is to expand basic action theories to basic contractual theories to provide the formal semantics of smart legal contracts to represent legal contracts as processes in the Situa- tion Calculus. Thus, we obtain an implementable specification that allows to automatically check many properties of the specification using an obligation-based GOLOG interpreter. Another Future work will enhance the current framework by inte- grating mechanisms to address norm violations and contrary-to- duty (CTD) obligations. Specifically, we intend to introduce explicit violation predicates to signify the non-fulfillment of primary obli- gations. Concurrently, we will define secondary obligations that are triggered by these violations. This will enable the model to rep- resent reparational duties and more accurately portray normative scenarios. Furthermore, we plan to explore the interplay between these augmented obligations and the underlying action theory of the Situation Calculus, alongside their application in legal reasoning and smart contract verification. References [1]Frank M Brown. 2014. The frame problem in artificial intelligence: Proceedings of the 1987 workshop. Morgan Kaufmann. [2] Jens Claรen and James P. Delgrande. 2020. Dyadic obligations over complex actions as deontic constraints in the situation calculus. In Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020, 253โ263. [3]Aspassia Daskalopulu. 2000. Modelling legal contracts as processes. In Proceed- ings 11th International Workshop on Database and Expert Systems Applications. IEEE, 1074โ1079. [4]Joost De Kruijff and Hans Weigand. 2017. Ontologies for commitment-based smart contracts. In OTM 2017: Confederated International Conferences: CoopIS, C&TC, and ODBASE 2017, Rhodes, Greece, October 23-27, 2017, Proceedings, Part I. Springer, 383โ398. [5]Robert Demolombe. 2004. From belief change to obligation change in the situation calculus. In Proceedings of the 16th Eureopean Conference on Artif. Intell., ECAIโ2004, PAIS 2004, Valencia, Spain, August 22-27, 2004. IOS Press, 991โ992. [6] Robert Demolombe and Andreas Herzig. 2004. Obligation change in depen- dence logic and situation calculus. In 7th International Workshop on Deontic Logic in Computer Science, DEON 2004, Madeira, Portugal, May 26-28, 2004. Proceedings 7. Springer, 57โ73. [7]Lucas Drumond and Rosario Girardi. 2008. A multi-agent legal recommender system. Artificial intelligence and law, 16, 2, 175โ207. [8] Guido Governatori, Francesco Olivieri, Erica Calardo, and Antonino Rotolo. 2016. Sequence semantics for norms and obligations. In Deontic Logic and Nor- mative Systems - 13th International Conference, DEON 2016, Bayreuth, Germany, July 18-21, 2018. Olivier Roy, Allard M. Tamminga, and Malte Willer, (Eds.) College Publications, 93โ108. [9]Guido Governatori and Antonino Rotolo. 2006. Logic of violations: A gentzen system for reasoning with contrary-to-duty obligations. Australas. J. Log., 4. doi:10.26686/AJL.V4I0.1780. [10]Sven Ove Hansson. 2006. Ideal worldsโwishful thinking in deontic logic. Studia logica, 82, 3, 329โ336. [11]Mustafa Hashmi, Guido Governatori, and Moe Thandar Wynn. 2014. Modeling obligations with event-calculus. In International Symposium on Rules and Rule Markup Languages for the Semantic Web. Springer, 296โ310. [12] Patrick J Hayes. 1981. The frame problem and related problems in artificial intelligence. In Readings in artificial intelligence. Elsevier, 223โ230. [13] Risto Hilpinen, (Ed.) 1970. Some main problems of deontic logic. Deontic Logic: In- troductory and Systematic Readings. Springer Netherlands, Dordrecht, Holland, 59โ104. [14] Jaakko Hintikka. 1971. Some main problems of deontic logic. In Deontic logic: Introductory and systematic readings. Springer, 59โ104. [15]Robert Kowalski and Marek Sergot. 1989. A logic-based calculus of events. In Foundations of knowledge base management. Springer, 23โ55. [16] Ronald M. Lee. 1988. A logic model for electronic contracting. Decis. Support Syst., 4, 1, 27โ44. doi:10.1016/0167-9236(88)90096-6. [17] Hector J. Levesque, Fiora Pirri, and Raymond Reiter. 1998. Foundations for the situation calculus. Electron. Trans. Artif. Intell., 2, 159โ178. http://w.ep.liu.s e/ej/etai/1998/005/. [18]Hector J. Levesque, Fiora Pirri, and Raymond Reiter. 1998. Foundations for the situation calculus. Electron. Trans. Artif. Intell., 2, 159โ178. [19]Hector J. Levesque, Raymond Reiter, Yves Lespรฉrance, Fangzhen Lin, and Richard B. Scherl. 1997. GOLOG: A logic programming language for dynamic domains. J. Log. Program., 31, 1-3, 59โ83. [20]Fangzhen Lin and Raymond Reiter. 1994. State constraints revisited. J. Log. Comput., 4, 5, 655โ678. [21]W. Bentley MacLeod. 2007. Reputations, relationships, and contract enforce- ment. Journal of Economic Literature, 45, 3, (Sept. 2007), 595โ628. doi:10.1257/j el.45.3.595. [22]John McCarthy. 1963. Situations, actions, and causal laws. Tech. rep. Stanford University, Dept of Computer Science. [23]Robert C Moore. 1981. Reasoning about knowledge and action. In Readings in Artif. Intell. Elsevier, 473โ477. [24]Fiora Pirri and Ray Reiter. 1999. Some contributions to the metatheory of the situation calculus. Journal of the ACM (JACM), 46, 3, 325โ361. [25] Fiora Pirri and Raymond Reiter. 1999. Some contributions to the metatheory of the situation calculus. J. ACM, 46, 3, 325โ361. [26] Henry Prakken and Giovanni Sartor. 2015. Law and logic: a review from an argumentation perspective. Artificial intelligence, 227, 214โ245. Obligation-Producing Actions in Situation CalculusLAWโ26 Legal Agent Workshop, June 2026, Singapore, Singapore [27]Raymond Reiter. 2001. Knowledge in action: logical foundations for specifying and implementing dynamical systems. MIT press. [28]Raymond Reiter. 2001. On knowledge-based programming with sensing in the situation calculus. ACM Trans. Comput. Log., 2, 4, 433โ457. [29]Raymond Reiter. 1991. The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression. In Artificial and Mathematical Theory of Computation, Papers in Honor of John McCarthy on the occasion of his sixty-fourth birthday. Vladimir Lifschitz, (Ed.) Academic Press / Elsevier, 359โ380. doi:10.1016/b978-0-12-450010-5.50026-8. [30]Raymond Reiter. 1991. The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. Artificial and Mathematical Theory of Computation, 3. [31] Richard B. Scherl and Hector J. Levesque. 1993. The frame problem and knowledge- producing actions. In Proceedings of the 11th National Conference on Artif. Intell., Washington, DC, July 11-15, 1993. AAAI Press, 689โ695. [32] Fรกbio Aiub Sperotto, Mairon Belchior, and Marilton Sanchotene de Aguiar. 2019. Ontology-based legal system in multi-agents systems. In Mexican International Conference on Artificial Intelligence. Springer, 507โ521. [33]G. H. von Wright. 1951. An Essay in Modal Logic. North-Holland Pub. Co., Amsterdam.