New directions in instantiation-based theorem proving

Harald Ganzinger, Konstantin Korovin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    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.
    Original languageEnglish
    Title of host publicationProceedings - Symposium on Logic in Computer Science|Proc Symp Logic Comput Sci
    Number of pages9
    Publication statusPublished - 2003
    Event18th Annual IEEE Symposium on Logic in Computer Science - Ottawa, Ont.
    Duration: 1 Jul 2003 → …


    Conference18th Annual IEEE Symposium on Logic in Computer Science
    CityOttawa, Ont.
    Period1/07/03 → …
    Internet address


    Dive into the research topics of 'New directions in instantiation-based theorem proving'. Together they form a unique fingerprint.

    Cite this