kirancodes.me
To Proof Maintenance & Beyond!

Controlled Natural Language Can Replace First-Order Logic

Norbert E. Fuchs, Uta Schwertel, Sunna Torge

Abstract

Many domain specialists are not familiar or comfortable with formal notations and formal tools like theorem provers or model generators. To address this problem, we developed Attempto Controlled English (ACE), a subset of English that can be unambiguously translated into first-order logic and thus can conveniently replace first-order logic as a formal notation. We describe how ACE has been used as a front-end to EP Tableaux, a model generation method complete for unsatisfiability and for finite satisfiability. We specified in ACE, a database example that was previously expressed in the EP Tableaux language PRQ, automatically translated the ACE specification into PRQ, and with the help of EP Tableaux reproduced the previously found results.

BibTeX
@inproceedings{Fuchs-al:ASE99,
  author    = {Norbert E. Fuchs and
               Uta Schwertel and
               Sunna Torge},
  title     = {Controlled Natural Language Can Replace {First-Order} Logic},
  booktitle = {ASE},
  pages     = {295--298},
  publisher = {{IEEE} Computer Society},
  year      = {1999},
}

Related papers