Logical English

Computer programs today are written in machine-oriented languages, which are not intelligible without computer training. As a consequence, many of the people who are affected by computer applications have little understanding of how those applications work and of the implicit assumptions that their implementations contain. People need to rely on informal, natural language specifications of the applications, and on the assurance of computer professionals that the applications correctly implement their specifications.

Ordinary natural language, on the other hand, is not only informal, but too ambiguous and too imprecise to serve directly as a computer-executable language. As a result, controlled natural languages (CNLs) have been developed to bridge the gap between ordinary natural language and computer executable languages. Many of these CNLs are based on formal logic, and are used for such applications as program specification, database queries and business rules.

This project will develop a logic-based CNL, Logical English (LE), inspired by the language of law, and suitable for executing legal documents, such as smart contracts. It will also aim to have the capabilities of a general-purpose computer language, using logical conditionals instead of conditional imperatives, and logical representations of time and change of state instead of assignment statements.

The underlying logic of LE will be an extension of logic programming, including types, functional expressions, weak and strong negation, reification and an amalgamation of object language and meta-language. The prototype of LE will be implemented in Prolog.

LE will use common nouns, such as “person” and “animal”, to represent types. The first occurrence of a typed logical variable will be preceded by an indefinite determiner, like “a” or “an”, and later occurrences in the same sentence by “the”. Different variables of the same type will be distinguished by the inclusion of an ordinal or other adjective between the determiner and the noun as in “a first person is an ancestor of a second person if the first person is a parent of an other person and the other person is an ancestor of the second person”.

The project will extend the existing design of LE, to include nested functional and relational expressions, as in “a first person is an ancestor of a second person if the first person is a parent of an ancestor of the second person”.

The logic of LE will also include an amalgamation of object level and metalevel predicates, which will allow modalities, such as obligation, to be represented by metalevel predicates, as in “it is obligatory that a first person pays a second person if the payment is specified in a transaction”. Notice the predicate “pays” in the conclusion of the sentence is nominalised as “the payment” in the condition of the sentence.

Because LE will be intelligible by readers without computer training, computer applications written in LE will have a much greater likelihood of being safe, trustworthy and reliable.

Project ID

STAI-CDT-2020-IC-12

Supervisor