Eighteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2003)

Paper: New Directions in Instantiation-Based Theorem Proving (at LICS 2003)

Authors: Harald Ganzinger Konstantin Korovin


We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests. We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are novel inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of successively refining the approximation.


    author = 	 {Harald Ganzinger and Konstantin Korovin},
    title = 	 {New Directions in Instantiation-Based Theorem Proving},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2003},
    year =	 2003,
    editor =	 {Phokion G. Kolaitis},
    month =	 {June}, 
    pages =      {55--64},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}