Norbert E. Fuchs, Uta Schwertel, Sunna Torge


    A Natural Language Front-End to 
Automatic Verification and Validation of Specifications

Often problem solving can be reduced to the search for finite
models of first-order logic specifications. We describe the model
generation method EP Tableaux that is complete for refutation and
for finite satisfiability. To make EP Tableaux available to domain
specialists unfamiliar with formal notations we added a natural 
language front-end that accepts Attempto Controlled English --- 
a subset of standard English with a domain-specific vocabulary 
and a restricted grammar. ACE allows users to express specifications 
precisely and in the terms of the application domain. ACE 
specifications are unambiguously translated into logic languages. 
We specified in ACE a database example that was previously specified 
in the EP Tableaux language PRQ, translated the ACE specification 
into PRQ, and reproduced the previously found results. As a further 
test, we formulated Schubert's Steamroller in ACE, translated the 
ACE version into PRQ and successfully proved the Steamroller's 
conclusions with EP Tableaux.