Link Search Menu Expand Document

Project Publications

The British Nationality Act as a logic program (Sergot et al. 1986)

Legal expert systemLegislation: executionLegislation: representation
dl.acm.org/doi/abs/10.1145/5689.5920
Main research: March 2022

Contents

  1. What does it claim to do?
  2. Substantiation of claims & potential issues
  3. How might the end-user assess effectiveness?
  4. What form does it take?
  5. The creators
  6. Jurisdiction

What does it claim to do?

This proof-of-concept is a formalisation of parts of the British Nationality Act 1981. It uses the Prolog language and an extended form of Horn Clause Logic. Its authors are computer scientists, whose goal was to combine :logic programming with law, such that the ‘executable’ version of the 1981 Act might yield insights about the implications of the legislation. It was not intended as a production system, nor as a complete representation of the 1981 Act.

Claimed essential features

  • Determine the consequences of the British Nationality Act (BNA) computationally, with explanations.
  • Expresses the Act in an accessible form.

“our translation of the act can be executed as a program by an augmented Prolog system, so that consequences of the act can be determined mechanically.” (Sergot et al. (1986), p. 370)

Knowledge expressed in logical form “is easy for both naïve users and experts to understand, is easy to modify … and allows the inference procedure to interact naturally with the human user and to explain its conclusions” (ibid., p. 383)

Claimed rationale and benefits

  • To use logic programming to make better sense of the British Nationality Act’s consequences.

    “We hoped that formalization of the various definitions might illuminate some of the issues causing the controversy [around the Act].” (p. 370)

    The Act is “relatively self-contained, and free, for the most part, of many complicating factors that make the problem of simulating legal reasoning so much more difficult. Furthermore, at the time of our original implementation (summer 1983) the act was free of the complicating influence of case law.” (p. 370)

  • To aid the drafting of legislative rules.

    “…an executable, logic-based representation of rules and regulations can be used not only to apply the rules, but to aid the process of drafting and redrafting the rules in the first place.” (p. 371)

    “Representation in logical form helps to identify and eliminate unintended ambiguity and imprecision … clarify and simplify the natural language statement of the rules themselves … derive logical consequences of the rules and therefore test them before they are put into force.” (p. 371)

  • To enable mechanical application of legal rules.

    The aim is to “concentrate on the limited objective of implementing rules and regulations with the purpose of applying them mechanically to individual cases.” (p. 372). The authors stress that “we have not addressed the broad and much more difficult problem of simulating legal reasoning” (pp. 371-2)

Claimed design choices

  • Uses the Prolog programming language.

    “Although Prolog logic is severely restricted, it proved to be sufficiently high level so that our implementation could resemble the style and structure of the actual text of the act. Such a resemblance is important because it helps increase confidence in the accuracy of the implementation and makes the implementation easier to maintain as the legislation changes and as case law evolves to augment the legislation.” (p. 370)

  • Uses Extended Horn Clause logic.
  • Uses backward chaining, reasoning backward from conclusion to conditions.
  • Rule conditions (‘subproblems’) can be resolved by various means, e.g. other rule results, end-user input, calculation.

  • High-level legal concepts (e.g. ‘good character’) are represented as binary conditions to be confirmed by external input.

    “This is a complete reversal of the normal approach to the development of axiomatic systems. The normal methodology starts with a primitive set of concepts and axioms. Higher level concepts are defined bottom up in terms of lower level ones that are primitive or have already been defined.” (p. 378)

  • Uses an expert system shell (APES) to ask the end-user questions, and provide explanations.
Top

Substantiation of claims & potential issues
  • The Act is treated as a single instrument, independent of other legal provisions that could in practice have a bearing on its legal interpretation or legal effects, particularly over time.
  • As the authors acknowledge, the “complicating influence of case law” is not represented, meaning judicial interpretations are not reflected in the coded rules.
  • The system requires input from the end-user regarding “vague concepts”. The meaning of concepts can only be authoritatively decided by the courts or relevant tribunals. Outputs based on end-user interpretations might not reflect those authoritative interpretations, which could have an impact on any legal effects that result from the output.
  • Despite the authors’ acknowledgement of the system’s limitations, there may be a risk that this kind of approach is used to formalise areas of law that are necessarily too complex or ambiguous for the kind of deductive reasoning the system is capable of.

Data

Data representation

  • The system uses Extended Horn Clause Logic (Sergot et al. (1986), p. 379):

    • conclusion <- condition1, condition2, … conditionn
  • Uses backward-chaining: “Figure 4 shows how Prolog proves theorems by reasoning backwards from conclusion to conditions” (ibid., p. 378; see Figure 1 above)

  • The representation is done using Prolog

    • Prolog is nondeterministic (cf. imperative programming); the proof of a rule outcome can be deduced in more than one way, all of which the system explores (ibid., p. 378)

    • The order of satisfaction of conditions is determined by the programmer (ibid., p. 378)

    • By the results of other rules within the same formalisation,
    • By accessing data (‘degenerate rules’ that state a single, unconditional proposition, e.g. ‘y is a Dependent Territory’),
    • By asking the end-user for a fact, e.g a name or date,
    • By means of computation, e.g. calculating if a date comes before/after another,
    • By asking a domain expert, e.g. a lawyer with knowledge of other relevant legislation, or another formalisation. (ibid., p. 378)

  • A number of assumptions are made about the data:

    • “The formalization of legislation results in an axiomatic theory that represents the legislation … Because the formalization of the British Nationality Act is an axiomatic theory, any logical consequence of the axiomatization can, in theory, be derived by means of a complete mechanical theorem prover.” (ibid., p. 376)

    • Closed World Assumption: facts which are not known are assumed to be false, thus the system treats them as though they are negations (“If we cannot show that an individual is excepted, then it is natural to assume that he or she is not excepted” (ibid., p. 379)); a ‘Negation as Failure’ assumption

      • To avoid this assumption would entail the need to reason with “all of first-order logic” and ordinary negation (i.e. without the assumption that unknown = false), instead of the more limited but more efficient extended Horn Clause Logic (ibid., p. 379).

      • This is thought to be an acceptable assumption, since “there are many instances where the legislation explicitly specifies all the cases for which a given predicate is intended to hold, and where the interpretation of negation as failure can safely be made” (ibid., p. 380)

      • Vague concepts (e.g. ‘good character’) can be bracketed and confirmed via user input, thus avoiding the problem of integrating such concepts into the representation itself (ibid., p. 371)

Resources

  • The paper itself: MJ Sergot et al., “The British Nationality Act as a Logic Program” (1986) 29 Communications of the ACM 370
  • A simpler version of the above paper: M Sergot et al., “Formalisation of the British nationality act” (1986) 2(1) International Review of Law, Computers & Technology 40-52
  • On the APES shell: P Hammond and MJ Sergot, ‘A PROLOG shell for logic based expert systems’. In Proc. BCS Conference on Expert Systems (1983, vol. 83, pp. 95-104).
Top

How might the end-user assess effectiveness?

The paper describes various test-cases the authors used to assess the efficacy of the system. It also discusses the limitations of the approach, highlighting some points where the intent of the legislation is not readily represented, or is actively reversed, by the logical constraints of the formalisation’s design. These are mitigated through augmentations of the approach that are based on certain assumptions continuing to hold.

The formal method aspects of Prolog allow for proofs to be made of the included rules, but the assessment from the perspective of an end-user will always be in terms of checking that the output matches a court’s understanding of the legislative text.

Top

What form does it take?

Form

Proof-of-concept

Details

The specific system that was build is pre-tailored to the rules contained in the British Nationality Act 1981, but of course the underlying methodology could be applied to any legislation capable of being represented with this kind of formalisation.

Top

The creators

Created by

Academics

Details

The authors are or were all computer scientists, some of whom went on after this paper to have distinguished careers in computer science and formal logic.

Top

Jurisdiction

Background of developers

United Kingdom

Target jurisdiction

United Kingdom, though again the formalisation method is not limited to a single jurisdiction.

Target legal domains

Immigration (the system is a formalisation of parts of a single UK Act), though the formalisation method is not limited to a single domain.

Top

Updated Top