Literature Review: Smart Contract Semantics <s> Lee's Adaptation of the RU Calculus <s> Abstract: Contracting is an essential aspectof doing business. Electronic contracting uses telecommunications and artificial intelligence to improve contracting processes by streamlining red tape enforcing legal correctness. To do this, the underlying conceptual structures of contracts and contracting must be carefully understood. A logic model is presented that emphasizes temporal, deontic and performative aspects of contracting. <s> BIB001 </s> Literature Review: Smart Contract Semantics <s> Lee's Adaptation of the RU Calculus <s> Implementing smart contracts to automate the performance of high-value over-the-counter (OTC) financial derivatives is a formidable challenge. Due to the regulatory framework and the scale of financial risk if a contract were to go wrong, the performance of these contracts must be enforceable in law and there is an absolute requirement that the smart contract will be faithful to the intentions of the parties as expressed in the original legal documentation. Formal methods provide an attractive route for validation and assurance, and here we present early results from an investigation of the semantics of industry-standard legal documentation for OTC derivatives. We explain the need for a formal representation that combines temporal, deontic and operational aspects, and focus on the requirements for the temporal aspects as derived from the legal text. The relevance of this work extends beyond OTC derivatives and is applicable to understanding the temporal semantics of a wide range of legal documentation. <s> BIB002
Lee's BIB001 framework for modelling absolute temporal expressions is based on the Rescher and Urquhart temporal logic system. In this system we have the R operator, with R t φ meaning that φ is realised at time t. In addition, a total ordering of times is introduced, allowing for absolute time references. Lee expands on this system by introducing notation to allow for the representation of time spans, and to denote when an some event is realised during a time span. This is crucial for use in smart contracts. In Lee's model, this temporal framework is integrated with deontic logic to represent deadlines (i.e. obligations with some fixed due date) and ongoing prohibitions. Lee BIB001 acknowledges some shortcomings of this model. First, he notes that the model assumes that the base time units used are equal in length, which is problematic if months or years are desired as a basis. Second, the system cannot handle continuous time. Clack and Vanca BIB002 identify some issues with Lee's framework. One criticism is that the system cannot handle all of the complex or nuanced temporal expressions that sometimes arise in the natural language of legal text. For example: in Lee's framework, there is no way of expressing "business days". Another example: it is difficult to express the set of dates corresponding to "the first Friday of every month" without directly specifying each day itself. Vanca  identifies one further issue with the model: the user is forced to choose some base unit of time for the system. This could prove problematic in cases where different contracts that use the same system are dealing with vastly different timescales. Vanca contrasts the example of a web hosting company that promises service uptimes with millisecond precision to derivatives contracts that deal with infrequent payments over many years.