Controlled Natural Language Input

Attempto Controlled English (ACE)

• A controlled natural language, i.e. a subset of English
• Can be unambiguously translated into first-order logic

Linking to the TPTP

• ACE to DRS translation by ACE parser (service in Zurich)
• DRS to TPTP translation by ACE tool or NACE
• ACE is an input language option in SystemB4TPTP
• Results passed to ATP ... a front end for SPASS-XDB

Examples

• Oedipus and Patricide

  Iokaste is a parent of Oedipus.
  Iokaste is a parent of Polyneikes.
  Oedipus is a parent of Polyneikes.
  Polyneikes is a parent of Thersandros.
  Oedipus is a patricide.
  Thersandros is not a patricide.
  Therefore, Iokaste is a parent of a patricide that is a parent of somebody who is not a patricide.

• Grocers aren't Cyclists

  If
  every honest and industrious person is healthy, and
  no grocer is healthy, and
  every industrious grocer is honest, and
  every cyclist is industrious, and
  every unhealthy cyclist is dishonest, and
  no healthy person is unhealthy, and
  no honest person is dishonest, and
  every grocer is a person, and
  every cyclist is a person
  then
  no grocer is a cyclist.

• Aunt Agatha

  Someone who lives in DreadburyMansion kills AuntAgatha.
  If somebody X lives in DreadburyMansion then X is AuntAgatha or X is the Butler or X is Charles.
  Everyone hates everyone that he kills.
  Noone is richer than someone that he kills.
  Charles hates noone who is hated by AuntAgatha.
  AuntAgatha does not hate the Butler.
  Everyone that is not the Butler is hated by AuntAgatha.
  The Butler hates everyone who is not richer than AuntAgatha.
  The Butler hates everyone who is hated by AuntAgatha.
  Noone hates everyone.
  AuntAgatha is not the Butler.
  Therefore, AuntAgatha kills AuntAgatha.

See the ACE project online