4. Motor Insurance Clause Example

Entity Relations, Ontology Inference, and Predicate Logic Syntax

See the L4 code for this ‘Motor Insurance’ example

This example is taken from the Compk Language Benchmark. The example proper begins at “Motor Breakdown Policy”.

This example is too long to be reproduced here. Instead, you will find notes on how to read and navigate the example. We hope the previous examples together with the notes below provide enough guidance to read this L4 formalisation of a motor insurance clause.

Remember that you can expand and collapse sections of the L4 encoding through the “+” and “-” signs found to the far left of the spreadsheet.

The Structure of the Motor Insurance Clause

The motor insurance clause is split into four major sections. The L4 formalisation of these sections are aligned with the relevant legal clauses found on the right of the page.

  1. § Motor Breakdown Policy

  • This line names the policy being formalised.

  1. §§ Meaning of Words

  • This section defines the meaning of the terms used in this contract. It is divided into several subsections marked by “§§§”. The subsubsections “Excess Satisfied” and “Excess Required” are subsubsections marked by “§§§§”. This is the longest part of the formalisation.

  1. §§ Section B - Misfuelling

  • This section consists of the conditional clause that determines when and what the insurer pays for.

  1. §§ Section C - General Exclusions

  • This section details the situations which the insurer will not pay for.