Skip to content

Latest commit

 

History

History
29 lines (22 loc) · 2.55 KB

formal_model.md

File metadata and controls

29 lines (22 loc) · 2.55 KB
Raw
date tags
2020-06-17
concept

Formal model

Real {contracts,programs} are large and complex. They are written in an unsuitable language for formal representation, e.g. {English,Python}.

To make it easier to test/reason about {contracts,programs}, we can build a model in some formal language. This model is a simplification of the underlying {contract,program}.

"All models are wrong, some are useful".

Languages in which to build models about contracts

  • Logics:
    • Deontic logic
    • Propositional dynamic logic
  • Lee (1988) A logic model for electronic contracting
  • Peyton Jones and Eber (2003) How to write a financial contract A combinator library in Haskell for representing [[[financial_contract]]].
  • Milosevic et al. (2004) Business Contract Language "A BCL contract consists of a set of roles along with a set of policies […] The roles define the parties involved in a contract, and the policies define the obligations and rights agreed upon by the parties. […] Governatori and Milosevic [36] later seek to formalise BCL by mapping it to a fragment of deontic logic extended with contrary-to-duty obligations. "
  • Prisacariu, Schneider (2009): Contract Language "a logic for expressing electronic contracts based on a combination of deontic, dynamic, and temporal logics. "
  • Martínez et al. (2010): C-O diagrams
  • Gulliksson, Camilleri (2016): Simplified Contract Language
  • Haeusler et al. (2010) Intuitionistic ALC (iALC) Explanation: ALC is one of the core Description Logics. ALC is extended with intuitionistic logic, because "Classical negation forces the negation of a proposition to be part of a concept, but in the context of “the law” the negation of a valid law does not have to be valid either. Besides the ontological complexity of dealing with legal statements together with non-legal ones by defining concepts that are outside jurisprudence, Classical negation can lead to unnecessary incoherent situations […]"