📄 A bidirectional mapping between English and CNF-based reasoners

Summary

Abney argues that if language maps between sound and meaning, interpretation should aim at the representation general cognition actually uses. He treats automated reasoners as the most explicit available models of cognition, and these usually take Clause Normal Form (CNF) as input. The textbook procedure for turning FOPC into CNF cannot be run backwards, so a reasoner's conclusions have no route back into English. His fix drops lambda-based bottom-up composition. Instead, selected nodes of the English LF tree are annotated with CNF operators, so one tree carries paired labels, with English words and CNF literals sitting together at the leaves. A feature grammar with atomic values only generates these trees. Variables travel as syntactic indices through concord-like rules, and negation lowering becomes a polarity feature checked locally. Parsing English produces CNF. Parsing an unordered set of literals, guided by their partial structure, produces English. The work is theoretical and reports no corpus or metrics. Its claimed benefits are an invertible interface to reasoners, a reduced form of Shieber's logical-equivalence problem (because CNF is a normal form), and donkey anaphora falling out of Skolemization.

Key points

• Running example: Kim feeds every stray cat pairs with the clause −S(x) ∨ −C(x) ∨ F(k, x). In this tree, determiner every is raised to head the quantifier-raising structure.
• Index propagation follows five rules:
  • a trace copies its antecedent's index;
  • a modifier copies the index of what it modifies;
  • a function word (auxiliary, case marker, case-marking of) copies its complement's index;
  • an argument discharges the last index of its argument-taker;
  • a parent inherits its head's undischarged indices.
• These rules sit alongside an Intrinsic Indices constraint: every non-pleonastic DP has an index.
• Polarity constraint: the root is positive, and only negation and the first child of → flip polarity. Under this rule, ¬(P ∨ (Q ∧ ¬R)) is read as −P ∧ (−Q ∨ R).
• The standard conversion has four steps: rewriting conditionals, lowering negation, Skolemization, and distribution. Abney aims to express all of them as feature constraints without restructuring the LF tree.
• Open problems:
  • Generalized quantifiers need reification with ↔, which breaks structure preservation.
  • Some CNF inputs have several maximally-consolidated forms, e.g. (P∨Q)∧(Q∨R)∧(R∨P).
• MRS is judged not genuinely flat and does not ease the equivalence problem.

Interesting ideas

• I1. A single tree whose nodes carry a pair of labels (surface and logic) lets one grammar run in both directions, avoiding a separate generator.
• I2. Instead of lambda terms, variables are passed as syntactic indices by local agreement rules (modifier, trace, function word, head inheritance), which keeps the mapping invertible.
• I3. Negation scope is computed by putting a polarity feature on every node, flipped only by negation and the antecedent of a conditional, so no tree rewriting is needed.
• I4. Mapping meanings to a canonical normal form makes many logically equivalent paraphrases collapse into one object.
• I5. Generation from an unordered set of literals is treated as ordinary parsing, with the known partial structure (which clause a literal belongs to) used as a constraint that prunes the search.

For Mova

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

• I1 (back): Frame/world graph nodes could stay anchored to UD tree nodes as paired labels, so generation means re-parsing the meaning side against the same grammar rather than inventing text from scratch.
• I2 (frames): Role filling could be written as explicit index-sharing rules over UD relations (amod, aux, case, obj), giving a traceable reason for every argument slot instead of opaque composition.
• I3 (world): Each asserted state or event could inherit a polarity from its path to the root, so negated or conditional facts are never stored as plain truths in the text's world.
• I4 (answer): Normalizing both a reader's answer and the gold meaning into a canonical clause-like form before comparison would let tests accept paraphrased but equivalent answers.
• I5 (back): The text→graph→text compressor could treat graph clusters as hard bracketing constraints during surface realization, reducing ordering ambiguity.