Translations of legal contracts into formal specifications that can be used for assisted reasoning are currently gaining considerable attention in AI and law. Yet, the conceptual intricacy of some of the normative notions involved in legal contracts continues to provide significant challenges to formalization; in accordance with this, there is a need for developing general logic frameworks which allow for an appropriate analysis of the fundamental components of a contractual situation. In the present work, we focus on the representation of decisional and operational roles played by possibly distinct contracting parties. We provide a flexible framework, which extends term-modal logic, where such roles can be efectively formalized and emphasized.
The formal analysis of legal contracts is an interdisciplinary area drawing attention from an increasing
number of researchers. For a recent and systematic review of approaches ofered in the literature, see
Soavi et al. [
Once one obtains a formal language that tracks all necessary concepts of a contract and a deductive
theory that handles both semantic relations and assumptions about scenarios regulated by the contract,
one can proceed further by automating reasoning tasks and/or creating a tool for user assistance. As
noted in [
We can briefly illustrate the diference between decisional roles and operational roles in a contract via an example. Suppose that Anna, a student, wants to spend a period of one month at a university in a foreign country and that she looks for an accommodation via a company called Student Housing. Such a company happens to have a flat for Anna, which can be booked under the following condition: a guarantor from Anna’s home institution is required to pay a deposit of 200e via online transfer to an account associated with Student Housing at a banking institution called InterBank. For our purposes we can neglect the additional condition that Anna will have to pay the rest of the rental fee by a certain date. Anna accepts these conditions, finds a suitable guarantor in Prof. Benvenuti and stipulates a legal contract with Student Housing including, among other things, all the information mentioned above.
Now, let us look at the parties emphasized in the example and the roles they play: Anna is the tenant, Student Housing is the flat owner , Prof. Benvenuti is the guarantor and InterBank is the payment addressee. The tenant and the flat owner are decisional roles, since the parties playing these roles stipulate the contract at issue. By contrast, the guarantor and the payment addressee play operational roles, since they are involved in the execution, rather than in the stipulation, of the contract.
In principle, the same roles could be played by diferent parties in similar circumstances (another student interested in renting another flat with another company, etc.). Thus, when we want to design a formal specification for this type of contract, it is convenient to keep track of the mentioned roles. More generally, every type of contract brings with it certain decisional and operational roles that are crucial to understand its content and that are invoked when one wants to check whether the contract was fulfilled or violated (e.g. the guarantor did not pay the deposit by the given deadline).
Here we propose a formal framework that emphasizes the distinction between decisional and operational roles in a contract and show its advantages over a standard representation in first-order (deontic) logic. Our framework is an extension of term-modal logic, introduced by Fitting, Thalmann and Voronkov [6], applied to normative reasoning by Frijters, Meheus and Van De Putte [7] and further developed in that context by Frijters [8, 9].
Term-modal logic (hereafter, TML) is an extension of first-order logic (hereafter, FOL) by means of indexed modal operators of the form □ , where is a finite list of terms (individual variables or constants). These terms stand for normative parties and □ will here represent a deontic operator of obligation. The additional expressiveness of TML in comparison to FOL allows one to formally capture the distinction between quantification over terms that occur as indices of a modal operator and quantification over terms that occur in the scope of a modal operator. Such a distinction is exemplified by the occurrences of and in the TML-formula below:
∀((Doctor() ∧ PatientOf(, )) → □ Cure(, )) We can read the whole formula as “for every and , if is a doctor and is a patient of , then it is obligatory for towards that cures ”. In other words, every doctor has an obligation towards their patients to cure them. The occurrences of and as indices of □ in the formula at issue convey an agent-directed obligation, rendered by the natural language expression “for towards ” which could not be directly captured in the language of (modal) FOL, as discussed in [8]. Clearly, being associated with a direction is a fundamental feature of many obligations. Usually, if we change the direction of an obligation, we give rise to a completely diferent norm. For instance, replacing □ with □ in the TML-formula above yields the (odd) reading that it is obligatory for patients towards doctors that the latter cure the former.
Our extension of TML will be called layered term-modal logic (hereafter, LTML) and is inspired by the following observation, made by Novotná and Pascucci in [10]. Norms are often not reducible to directed obligations; they rather result from an agreement or a contract: some parties stipulate that other (possibly diferent) parties have to behave a certain way. Thus, a norm can conceptually be analysed as a structure involving two layers of parties: one includes those parties that stipulate the agreement (i.e. play decisional roles), the other those parties that are expected to act in accordance with the agreement (i.e. play operational roles).
Let = {, , . . .} be a countable set of individual constants and = {, , . . .} a countable set of individual variables, where , , . . . range over and , , . . . over . Let = ∪ be the set of terms and , , . . . the metavariables ranging over it. We use 1, 2, . . . to refer to finite ( possibly empty) lists of terms. Let Σ, for ∈ N, denote the set of all lists of terms with cardinality and Σ the union of all Σ. We take = ⟨ 1, . . . , ⟩ and ∀ as an abbreviation for ∀ 1 . . . ∀ . Finally, for ∈ N, let be a countable set of -ary predicate symbols and denote the union of all .
LTML-formulas are defined as below, where ∈ , 1, 2, 3, 4 ∈ Σ, , ∈ , and ∈ : We take symbols ⊤, ⊥, ∧, →, ↔ and ∃ to be defined in a standard way. We write ̸= as an abbreviation for ¬ = . Parentheses are omitted whenever possible. Free and bound variables in formulas are defined as usual, with one addition: the free variables in Δ(( 31⇒⇒ 42)) are all the variables that occur free in and all the variables that occur in 1, 2, 3 and 4. A formula is a sentence if all variables in are bound. We use Sent for the set of all LTML-sentences.
The additional expressiveness of LTML in comparison to FOL is given by the following features: for every four lists 1, . . . , 4 of terms, we have the operators Δ(( 31⇒⇒ 42)) and Δ(( 31̸⇒⇒ 42)), which take a formula as input and give a formula as output. These operators were introduced in [10] within a propositional framework. They can be regarded as special term-modal operators, given that they are modal operators indexed with a quadruple of lists ( 1, . . . , 4) grouped into two layers. In the present context, the upper layer indicates parties playing decisional roles, whereas the lower layer indicates parties playing operational roles. Moreover, each layer has a direction thanks to the presence of symbols ⇒ and ̸⇒. We will call Δ(( 13⇒⇒ 24)) and Δ(( 13̸⇒⇒ 24)) layered term-modal operators (or LTML-operators).
The flexible reading of these operators can be explained by examining some schemata of formulas. If none of the lists 1, . . . , 4 is empty, we get the interpretation in Table 1:
Formula
Reading Δ(( 13⇒⇒ 24)) Δ(( 13̸⇒⇒ 24)) on the basis of a stipulation of 1 relevant to 2, 3 must bring about towards 4 on the basis of a stipulation of 1 relevant to 2, 3 must avoid bringing about towards 4 This reading indicates that 1 and 3 (which occur to the left of arrow symbols) are lists of normative parties playing active roles, while 2 and 4 (which occur to the right of arrow symbols) are lists of normative parties playing passive roles. Normative parties can also be said to be legal agents, where these are not necessarily individual agents (e.g. sometimes a legal agent is an institution like a bank). Notice, however, that the same party can play both an active role and a passive role, as well as occur both in the upper layer (decisional) and in the lower layer (operational). For instance, consider the occurrences of or of in the following schema: Δ((,,⇒⇒,)). Accordingly, given that most legal contracts are such that all agreeing parties play both an active decisional role (being involved in the stipulation) and a passive decisional role (being afected by the fulfilment/violation of the contract), it is often the case that 1 and 2 are the same lists of parties. In those cases, one can adopt a graphical convention and write e.g. Δ((,⇒⇔),), with a bidirectional arrow which emphasizes the reciprocity of the contract at the decisional level. We can use an instance of the latter schema to interpret the working example from section 2: we assume that is Anna (tenant), is Student Union (flat owner), is Prof. Benvenuti (guarantor), is InterBank (payment addressee) and let = PayOnline(200e) describe the fact that 200e are paid via online transfer. The whole can be read in accordance with Table 1, namely: on the basis of a stipulation between Anna and Student Union, Prof. Benvenuti has to pay 200e via online transfer to InterBank.
In order to move from the representation of a specific contract to the representation of a type of contract, we add role-labels to the positions occupied by indices of an LTML-operator, so as to obtain an interpreted pattern of LTML-operator. In this regard, consider the type of contract instantiated by the working example. We identified four fundamental roles in the working example (tenant, flat owner, guarantor and payment addressee). We can thus define the following conditions on an operator Δ(( 13⇒⇒ 24)): both 1 and 2 is an ordered pair of terms (the same pair), where the first term plays the role of and the second term plays the role of ; 3 consists of a single term playing the role of ; finally, 4 consists of a single term playing the role of . The result is an interpreted pattern of LTML-operator where we can use any indices diferent from , , and to formalize a new instance of the same type of contract mentioned in the working example. Diferent types of contracts will be associated with other interpreted patterns of LTML-operators. In other words, we can always introduce a new set of role-labels to build interpreted patterns of LTML-operators, depending on the sort of legal contract that we want to analyse.
If some of the lists of terms in an LTML-operator are empty, the reading of the formulas in Table 1 can be changed accordingly. For a systematic analysis of all possible cases, see [10]. For instance, if 1 = ∅ and 2 ̸= ∅, we are representing a norm based on the fulfillment of a condition (e.g. a norm applicable to the category of self-employed workers), if 1 ̸= ∅ and 2 = ∅ we are representing a unilateral decision (e.g. a norm resulting from a judicial decision). If 1 = 2 = ∅, then the decisional layer is vacuously mentioned, and we are ultimately representing a norm without any reference to its source (e.g. the simple command “Carla ought to pay a rental fee to Emma”). An empty list of terms in an LTML-operator will also be denoted by a blank space. Moreover, * will denote either ⇒ or ̸⇒.
The deductive relevance of empty lists of terms in LTML-operators is clarified via the notion of reference-abstraction, which indicates how one can safely perform an inference from a norm 1 contained in a legal contract to a simpler norm 2 by removing (some) reference to some of the parties involved in 1, either at the decisional level or at the operational level. Notice that any norm which is inferred by following this procedure applies to the same legal context as the original norm. For instance, saying that Prof. Benvenuti ought to pay 200e to InterBank due to an agreement between Anna and Student Union implies that Prof. Benvenuti ought to pay 200e due to an agreement between Anna and Student Union. In performing such an inference, the important point to keep in mind is that the latter norm should be interpreted in a context-relative way, namely as based on the information available in the particular contract analysed. We cannot apply the inferred norm to arbitrary circumstances. To better illustrate the idea of context-relativity, it is convenient to look at an even simpler norm that we can infer in the working example, namely that Prof. Benvenuti ought to pay 200e. Such a norm says something about the specific legal scenario analysed and should not be confused with the absolute norm according to which Prof. Benvenuti ought to pay 200e under any circumstances and to an arbitrary party.
Another noteworthy aspect of operators endowed with indices of normative parties and with a direction, like our operator Δ(( 13⇒⇒ 24)), is that they can be used to express Hohfeldian concepts and their relations; this aspect is more extensively discussed in [10]. In particular, consider the correlativity of rights and duties: has a duty towards if has a right against . Under this view, the fact that Prof. Benvenuti ought to pay 200e to InterBank can be interpreted both as a duty of Prof. Benvenuti towards InterBank and as a right of InterBank against Prof. Benvenuti. Therefore, as far as the symbolic language is concerned, both these instances of Hohfeldian concepts can be expressed by the same formula.
Definition 1 (Reference-abstraction). Let 1 = Δ(( 31 ⇒* 24)); a reference-abstraction of 1 is any LTML-formula 2 obtained from 1 by removing some occurrence of an index in its main LTML-operator. The relation of being a reference-abstraction is taken to be transitive. Thus, Δ((⇒⇒ )) is a referenceabstraction of Δ((,,⇒⇒)) and Δ(( 13⇒⇒ )) is a reference-abstraction of Δ(( 31⇒⇒ 42)).1
We provide a semantics for LTML based on neighborhood models. For a related semantics in the case of TML, see Frijters and Van De Putte [11]. We stress that reference-abstraction is addressed by clause 3.1 of the following definition. Given a set , we take L( ) to be the set of all finite lists (sequences) over and 1( ) ⊑ 2( ) to mean that 1( ) is an order-preserving list formed by a subset of the objects in a list 2( ). In other words, 1( ) ⊑ 2( ) means that 1( ) and 2( ) are two lists over the same set and the former is obtained from the latter by possibly removing some objects (normative parties, in the present context).
Definition 2. An LTML-model is a tuple = ⟨, , , ⟩, where: 1. ̸= ∅ is the world domain of 2. ̸= ∅ is the agent domain of 3. : × L()× L()× L()× L() → ℘(℘( )) is the neighborhood function of , where: 3.1. if ∈ (, 1(), 2(), 3(), 4()), 1′() ⊑ 1(), 2′() ⊑ 2(), 3′() ⊑ 3() and 4′() ⊑ 4(), then ∈ (, 1′(), 2′(), 3′(), 4′()) 4. is an interpretation function of , where: 4.1. : → 4.2. : × → ℘() for every ∈ N such that ≥ 1.
4.3. : 0 → ℘( ) We stress that an -ary predicate is interpreted at each world as a set of -tuples of normative parties.
Given some model = ⟨, , , ⟩ and = ⟨ 1, . . . , ⟩, we will henceforth use ( ) as shorthand for the tuple ⟨ ( 1), . . . , ( )⟩. We call | | = { | ∈ and , |= } the truth set of . For any ∈ , ′ = ⟨, , , ′⟩ is a -alternative of = ⟨, , , ⟩ if ′ difers at most from in the member of that ′ assigns to .
Definition 3 (Semantic Clauses). For any LTML-model = ⟨, , , ⟩ and ∈ : SC1 If ∈ for some ≥ 1, then , |= ( ) if ( ) ∈ (, ) SC1’ If ∈ 0, then , |= if ∈ ( ) SC2 , |= ¬ if , ̸|= SC3 , |= ∨ if , |= or , |= SC4 , |= = if ( ) = ( ) SC5 , |= Δ 1⇒ 2 if | | ∈ (, ( 1), ( 2), ( 3), ( 4))
3⇒ 4 SC6 , |= (∀ ) if for every -alternative ′: ′, |= .
Definition 4. Let Γ ⊆ Sent and ∈ Sent: is a semantic consequence of Γ if for every LTML-model = ⟨, , , ⟩ and ∈ : if , |= for all ∈ Γ, then , |= . If Γ = ∅, then is valid. 1The TML-operators used in [6] correspond to LTML-operators of the form Δ(( 3⇒⇒ )) or Δ(( 1⇒ )), namely where only active roles in one layer are mentioned, while those used in [8, 9] could match LTML-operator⇒shaving any of the forms Δro((le1s,⇒⇒alt2h))o,uΔgh(( t3h⇒⇒ey4d))o, Δno((t 1ta⇒⇒ke4l))ayaenrds Δof((ro3l⇒⇒es i2n))t,ogaivcecnoutnhta.t they allow for a distinction between active roles and passive
An axiomatization of LTML on neighborhood models is obtained by closing an axiomatization of classical propositional logic under the principles in Table 2.2 As in [11], we use the following notation: (/ ) is the result of replacing all free occurrences of in by , renaming bound variables if necessary to avoid rendering new occurrences of bound in (/ ). (// ) is the result of possibly replacing some free occurrences of in by , again renaming something if necessary.
A formula ∈ Sent is a theorem of LTML (in symbols, ⊢ ) if can be derived from the axioms and rules of LTML. ∈ Sent is derivable from Γ ⊆ Sent in LTML (denoted Γ ⊢ ) if there are 1, . . . , ∈ Γ such that ⊢ ( 1 ∧ . . . ∧ ) → .
Label (UI) (REF) (SUB) (ABS)
Axiom Schema (∀ ) → (/ ) = ( = ) → ( → (// )) if is a reference-abstraction of , then → if ⊢ ↔ , then ⊢ Δ(( 31 ⇒* 24)) ↔ Δ(( 31 ⇒* 24)) to infer from the assumptions and → if ⊢ → (/ ) and neither occurs in nor in , then ⊢ → (∀ ) .
We emphasize that, in the axiomatic basis provided above, principle ABS gives rise to a form of Modus Ponens which captures the ideas behind reference-abstraction.
In this work, we presented an extension of term-modal logic called LTML (layered term-modal logic) and showed that it can properly account for the distinction between decisional roles and operational roles in a contract, which is a crucial component of legal reasoning. Our proposal combines intuitions put forward in [10] with a language whose expressiveness is higher than modal FOL. Our future inquiries in this area will be dedicated to the analysis of fragments of LTML that are suitable for an automated representation of selected types of contract and thus for the development of tools for assisted reasoning.
The following statement applies to Matteo Pascucci: This research was funded in whole or in part by the Austrian Science Fund (FWF) 10.55776/I6499. For open access purposes, the author has applied a CC BY public copyright license to any author-accepted manuscript version arising from this submission. 2Adding other principles such as aggregation or inheritance to the axiomatisation provided is straightforward; see [11]. [4] T. Libal, M. Pascucci, Automated reasoning in normative detachment structures with ideal conditions, in: ICAIL ’19: Proceedings of the 17th International Conference on Artificial Intelligence and Law, ACM, 2019, pp. 63–72. [5] A. Steen, D. Fuenmayor, Bridging Between LegalRuleML and TPTP for Automated Normative
Reasoning, in: RuleML+RR2022, Springer, 2022, pp. 244–260. [6] M. Fitting, L. Thalmann, A. Voronkov, Term-modal logics, Studia Logica 69 (2001) 133–169. [7] S. Frijters, J. Meheus, F. Van De Putte, Reasoning with rules and rights: term-modal deontic logic, in: New Developments in Legal Reasoning and Logic: From Ancient Law to Modern Legal Systems, Springer Cham, 2021, pp. 321–352. [8] S. Frijters, All doctors have an obligation to care for their patients: Term-modal logics for ethical reasoning with quantfied deontic statements., Ph.D. thesis, Ghent University, Ghent, Belgium, 2020. [9] S. Frijters, An Andersonian-Kangerian reduction of term-modal deontic logic, in: DEON 2023: Proceedings of the 16th International Conference on Deontic Logic and Normative Systems, College Publications, 2023, pp. 159–176. [10] T. Novotná, M. Pascucci, Normative parties in subject position and in object position, in: The
Logica Yearbook 2020, College Publications, 2021, pp. 147–164. [11] S. Frijters, F. Van De Putte, Classical term-modal logics, Journal of Logic and Computation 31 (2020) 1026–1054.