We present a first step towards a framework for defining and manipulating normative documents or contracts described as Contract-Oriented (C-O) Diagrams. These diagrams provide a visual representation for such texts, giving the possibility to express a signatory's obligations, permissions and prohibitions, with or without timing constraints, as well as the penalties resulting from the non-fulfilment of a contract. This work presents a CNL for verbalising C-O Diagrams, a web-based tool allowing editing in this CNL, and another for visualising and manipulating the diagrams interactively. We then show how these proof-of-concept tools can be used by applying them to a small example.
may be seen as a generalisation of @cite_0 @cite_13 @cite_11 in terms of expressivity. On the other hand, has three different formal semantics: an encoding into the @math -calculus, a trace semantics, and a Kripke-semantics. In a previous work, introduced a CNL for in the framework @cite_6 . allows for the verification of conflicts (contradictory obligations, permissions and prohibitions) in normative texts using the CLAN tool @cite_10 . The biggest difference between and the current work, besides the underlying logical formalism, is that we treat agents and actions as linguistic categories, and not as simple strings. This enables better agreement in the CNL which lends itself to more natural verbalisations, as well as making it easier to translate the CNL into other natural languages. We also introduce the special treatment of two-item co-ordination, and have a more general handling of lists as required by our more expressive target language.
@cite_13 @cite_6 @cite_0 @cite_10 @cite_11
2558511176 2141573378 2109740450 2150436779
This paper presents a new version of the CL contract speci- fication language. CL combines deontic logic with propositional dynamic logic but it applies the modalities exclusively over structured actions. CL features synchronous actions, conflict relation, and an action nega- tion operation. The CL version that we present here is more expressive and has a cleaner semantics than its predecessor. We give a direct seman- tics for CL in terms of normative structures. We show that CL respects several desired properties from legal contracts and is decidable. We relate this semantics with a trace semantics of CL which we used for run-time monitoring contracts. In this paper we are concerned with the analysis of normative conflicts, or the detection of conflicting obligations, permissions and prohibitions in normative texts written in a Controlled Natural Language (CNL). For this we present AnaCon, a proof-of-concept system where normative texts written in CNL are automatically translated into the formal language CL using the Grammatical Framework (GF). Such CL expressions are then analysed for normative conflicts by the CLAN tool, which gives counter-examples in cases where conflicts are found. The framework also uses GF to give a CNL version of the counter-example, helping the user to identify the conflicts in the original text. We detail the application of AnaCon to two case studies and discuss the effectiveness of our approach. In this paper we propose a formal language for writing electronic contracts, based on the deontic notions of obligation, permission, and prohibition. We take an ought-to-do approach, where deontic operators are applied to actions instead of state-of-affairs. We propose an extension of the µ-calculus in order to capture the intuitive meaning of the deontic notions and to express concurrent actions. We provide a translation of the contract language into the logic, the semantics of which faithfully captures the meaning of obligation, permission and prohibition. We also show how our language captures most of the intuitive desirable properties of electronic contracts, as well as how it avoids most of the classical paradoxes of deontic logic. We finally show its applicability on a contract example. We present a dynamic deontic logic for specifying and reasoning about complex contracts. The concepts that our contract logic CL captures are drawn from legal contracts, as we consider that these are more general and expressive than what is usually found in computer science (like in software contracts, web services specifications, or communication protocols). CL is intended to be used in specifying complex contracts found in computer science. This influences many of the design decisio ns behind CL. We adopt an ought-to-do approach to deontic logic and apply the deontic modalities exclusively over complex actions. On top, we add the modalities of dynamic logic so to be able to reason about what happens after an action is performed. CL can reason about regular synchronous actions capturing the notion of actions done at the same time. CL incorporates the notions of contrary-to-duty and contrary-to-p rohibition by attaching to the deontic modalities explicitly a reparation which is to be en forced in case of violations. Results of decidability and tree model property are given as well as specific properties for the modalities.