2. Deontic and Temporal Logic Examples¶

Contract As Automaton Example¶

Events & Consequences, Obligations vs Permissions¶

See the L4 Code for this ‘Contract As Automaton’ example

In the Must Sing Rule, we learned that we can use L4 to formalise a rule.

The rule was just about short enough to formalise without causing too much mental strain. But what happens when you need to formalise even longer rules, or rules with multiple sections that repeatedly use the same terms and rules?

This Contract as Automaton example will tackle this issue and teach you how to define terms and rules so that they can be inserted repeatedly in the main formalisation.

Our running example is a loan contract. A loan is repaid in two instalments. The borrower has to stay out of trouble.

The example comes from a paper by Mark D. Flood and Oliver R. Goodenough, pages 5 and 6.

Loan Agreement template and contract commencement¶

Consider the following section of the example:

The Loan

At the request of Borrower, to be given on June 1, 2014, Lender will advance $1,000 to Borrower no later than June 2, 2014. If Borrower does not make such a request, this agreement will terminate.

Explicitly stating abstract concepts with the DECLARE and HAS keywords¶

We need to explicitly state the abstract concepts that are needed to formalise this contract in L4. In this case, we need the concept of a ‘loan’. In L4, we can define a ‘loan’ like this:

DECLARE	Loan	IS AN	Agreement
HAS	Lender	IS A	Person
	Borrower	IS A	Person
	Closing	IS A	Date
	Principal	IS A	Money

We can split this table into two parts.

The first part consists only of the first row that has “DECLARE… Agreement”.

The second part consists of the rest of the rows, “HAS… Money”.

First, we explictly state, by declaring, an abstract thing called a ‘loan’, and that this ‘loan’ is an ‘agreement’. We chose not to explicitly declare what an ‘agreement’ is, but we could do so if needed.

Second, we explicitly state that something is a ‘loan’ only if it contains the items stated after the HAS keyword. In this example, only if there is a:

‘Lender’, who is a person,
‘Borrower’, who is also a person,
‘Closing’, that is a date,
‘Principal’, that is some amount of money…

…can we consider something a ‘loan’.

Creating objects that are a kind of abstract concept with the DEFINE keyword¶

We now have a rigorous definition of an abstract idea called a ‘loan’. But all we have now is this one abstract idea. In other words, there is currently no concrete object that is a ‘loan’.

Let’s create such a concrete object using the DEFINE keyword.

DEFINE	F_and_G	IS A	Loan
HAS	Mark	IS THE	Lender
	Oliver	IS THE	Borrower
	1 June 2014	IS THE	Closing
	$1000	IS THE	Principal

Similarly, we can split this table into two parts.

The first part consists only of the first row that has “DEFINE… Loan”.

The second part consists of the rest of the rows, “HAS… Principal”.

Notice that the definition of a concrete object follows the same pattern as when we declare an abstract idea.

First, we explicitly state, by defining, a concrete thing called an “F_and_G”, and that this “F_and_G” is a ‘loan’.

Second, we explicitly state that “F_and_G” has the following items:

“Mark”, who is the Lender
“Oliver”, who is the Borrower
“1 June 2014”, which is a Closing (date)
“$1000”, which is the Principal (money)

This “F_and_G” object satisfies the requirements to be a ‘loan’, and is therefore a ‘loan’.

Repeated use of defined terms and rules¶

This example shows how defined terms and rules can be defined separately and used in other rules.

In this case, Repayment is defined in a separate section and used in the main definition of the condition that needs to be fulfilled.

This example uses a slightly simplified example from the LegalSS spreadsheet and does not consider “§ Contract Commencement” on lines 41-48.

Condition to trigger Repayment¶
§	Condition
PARTY	Lender
MUST	remit principal
	in the amount of $1000
	to Borrower
WITHIN	1 day
HENCE	Repayment

The condition above says that the lender must remit a principal of $1000 to the Borrower within one day, or else (hence) Repayment will be triggered.

The “§” symbol is a section symbol which gives a name to the L4 section below the “§” symbol.

In this example, Repayment is defined as follows:

Definition of Repayment¶
§§	Repayment
	Repayment
MEANS	Main - Repay in two halves
AND	Side - Keep taxes paid

The definition of Repayment above says that the borrower has to repay the principal in two halves while also keeping their taxes paid.

Notice the use of the “§” symbol again, but this time with two of them together, “§§”. This means that this is a subsection, like a clause and subclause in law. If we follow the analogy, then “§” is, say, section 1, and “§§” is section 1.1.

In this case, “§§” means that the L4 section beneath “§§” can be inserted into any L4 section that has a “§” label.

The differences between DECIDE, DECLARE, and DEFINE¶

DECIDE is where you state explicitly what format you’ve chosen to formalise.

In the Home Insurance Clause, we decided to formalise a positive version of the contract, telling others that “the loss or damage is covered if…” instead of “the loss or damage is not covered if…”.
DECLARE is where you state explicitly what abstract concepts that are needed in formalising the contract. In this example, we need a concept of a ‘loan’, which is abstract because the idea of a ‘loan’ is a mental idea. But what exactly is a ‘loan’?

In this example, something is a ‘loan’ when there is a ‘Lender’ that is a person, a ‘Borrower’ that is a person, a ‘Closing’ that is a Date, and a ‘Principal’ that is Money.
DEFINE is where you state explicitly a collection of ‘stuff’ is actually a type of abstract concept.

In this example, the “stuff” is something called an “F_and_G” which is a ‘loan’ type. This “F_and_G” is a collection of ‘stuff’ you can point to, in this case, a “Mark” which is a Lender, an “Oliver” which is a Borrower, a “1 June 2014” which is a Closing, and “$1000” which is a Principal amount.