I hope that this document has been a clear introduction to the principles of Decision Procedures and their potential uses in computer software, and that it will stimulate further contributions from our affiliates and interest from other software developers.
It is intended that this document will be extended and elaborated as the project developes. Additional reports will also be produced describing progress with the domain case studies and DP implementations.
If a complete quantifier elimination procedure can be found for a 1st-order theory of some domain, this can be used to provide full 1st-order logic expressions (over a restricted non-logical vocabulary relevant to a particular domain) within a programming language. The user need only specify procedures to determine the truth values of atomic formulae. Quantified expressions can then be automatically evaluated and used, for example, in program statements of the form:
The workings of the quantifier elimination procedure would be completely hidden from the user, so that use of the system would only require an understanding of the meanings of 1st-order expressions.