CL - a logic for reasoning about legal contracts: - Semantics
Christian Prisacariu, Gerardo Schneider · NORA - Norwegian Open Research Archives · 2008
The work reported here is concerned with the definition of a logic (which we call CL) for reasoning about legal contracts. The report presents the syntax of the logic and the associated semantics. There are two se-mantics presented: one is defined with respect to linear structures (i.e. traces of actions) and is intended for run-time monitoring of executions of contracts; the second semantics is given over branching structures (i.e. Kripke-like structures) and is intended for reasoning about contracts in a static manner (i.e. model-checking and theorem proving). In the first part of the report we present the theoretical results underlying the branching semantics. It presents an algebra of actions and restates some of previous results presented in another report, as well as new results useful for the definition of the branching semantics and for the proofs. The rest of the report is concerned with the definition of the two semantics. Moreover, several (non-standard) desired properties of the logic are proven.