Complex quantifier elimination in HOL

John Harrison.

Supplementary proceedings of the 2001 International Conference on Theorem Proving in Higher Order Logics, pp. 159-174, 2001.

Abstract:

Building on a simple construction of the complex numbers and a proof of the Fundamental Theorem of Algebra, we implement, as a HOL derived inference rule, a decision method for the first order algebraic theory of C based on quantifier elimination. Although capable of solving some mildly interesting problems, we also implement a more efficient semidecision procedure for the universal fragment based on Gröbner bases. This is applied to examples including the automatic proof of some simple geometry theorems. The general and universal procedures present an interesting contrast in that the latter can exploit the finding-checking separation to achieve greater efficiency, though this feature is only partly exploited in the present implementation.

DVI or PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-complex,
        author          = "John Harrison",
        title           = "Complex quantifier elimination in {HOL}",
        editor          = "Richard J. Boulton and Paul B. Jackson", 
        booktitle       = "{TPHOLs} 2001: Supplemental Proceedings",
        publisher       = "Division of Informatics, University of Edinburgh",
        note            = "Published as Informatics Report Series 
                           EDI-INF-RR-0046. Available on the Web at 
     {\tt http://www.informatics.ed.ac.uk/publications/report/0046.html}", 
        year            = 2001,
        pages           = "159--174"}