📄 Reasoning in Attempto Controlled English: Mathematical and Functional Extensions

Summary

This paper is the last of three system descriptions covering RACE, the first-order reasoner for Attempto Controlled English (ACE). It closes the remaining gaps in RACE's coverage of ACE. Earlier RACE matched logical atoms by unification. That method fails for arithmetic, where expressions must be computed, evaluation may depend on values given later in the text, and conflicts can occur without any negation. To handle this, the author connects RACE to SWI Prolog's clpqr constraint library, so no change to ACE syntax is needed. Worked examples include an interest-and-fee banking calculation, a farmer word problem rewritten as linear equations, and quadratic equations such as the Golden Ratio. A second extension adds a list-based functional notation that lets ACE texts call Prolog predicates. This enables recursion, such as Euclid's gcd, and operations on lists, sets and strings. RACE now covers every ACE construct that has a first-order logic reading. The author also discusses two open problems: hidden formality and the relevance of the conclusions RACE draws.

Key points

• RACE supports consistency checking, textual entailment and query answering. Input is ACE, and output is ACE plus English. For each result it lists the minimal subsets of axioms that are inconsistent or that entail the theorem or query.
• About 100 auxiliary axioms supply domain-independent knowledge. They are written in Prolog over ACE's internal representation and are invoked only when needed.
• The arithmetic work had to handle four new phenomena, all addressed with clpqr:
  • values must be computed rather than unified;
  • evaluation must wait until operands are known;
  • formulas must be related to each other (X=1 entails X>0);
  • contradictions can arise without negation (A is 1 / A is 2, or 1=2).
• The farmer problem (100 animals, 260 feet) gives 30 cows and 70 ducks. Quadratic equations are solved by substituting the closed-form roots, with these restrictions:
  • the squared term has no coefficient;
  • P and Q are integers, fractions or reals;
  • complex roots raise an error.
• The functional syntax is ["functor", arg1, ...], with the functor written as a string so it needs no lexicon entry. An example combining append, max_list and min_list returns 7. RACE still excludes imperatives and the should/may modals from Clinical Practice Guidelines.

Interesting ideas

• I1. Instead of building arithmetic into the unification-based reasoner, the system hands numeric constraints to an off-the-shelf solver, which also handles deferred evaluation and order-independent facts.
• I2. Every answer comes with the minimal set of premises that supports it, a compact and checkable form of explanation.
• I3. A contradiction can be two incompatible values for the same quantity, with no negation involved.
• I4. The word problem becomes solvable only after hidden background facts are stated explicitly (every cow has 4 feet, no cow is a duck) and turned into equations.
• I5. The author separates logically valid conclusions from commonsense ones, such as inferring possession from "John's cat purrs", and notes that users disagree on whether the latter are acceptable.

For Mova

How these ideas could serve Mova, our small open language model — its files, stages and tests:

• I1 (answer): maths word problems could turn quantities from the text world into constraints for a CLP-style solver, so facts stated in any order still resolve.
• I2 (answer): fable QA and test readers could return the smallest set of world facts behind each answer, which also makes negative-control evaluation easier.
• I3 (world): state tracking could flag an entity attribute that receives two different values at the same time point as a conflict, not only explicit "not" statements.
• I4 (world): compiled knowledge about parts and counts per class (WordNet/Wikidata) could be injected automatically when a word problem aggregates quantities over categories.
• I5 (frames): implicature and possessive-derived inferences could be tagged as defeasible or commonsense, so later stages and users can see which conclusions are strict entailments.