Labelled unit superposition calculi for instantiation-based reasoning

Konstantin Korovin, Christoph Sticksel

    Research output: Chapter in Book/Conference proceedingConference contributionpeer-review

    Abstract

    The Inst-Gen-Eq method is an instantiation-based calculus which is complete for first-order clause logic modulo equality. Its distinctive feature is that it combines first-order reasoning with efficient ground satisfiability checking which is delegated in a modular way to any state-of-the-art ground SMT solver. The first-order reasoning modulo equality employs a superposition-style calculus which generates the instances needed by the ground solver to refine a model of a ground abstraction or to witness unsatisfiability. In this paper we present and compare different labelling mechanisms in the unit superposition calculus that facilitates finding the necessary instances. We demonstrate and evaluate how different label structures such as sets, AND/OR trees and OBDDs affect the interplay between the proof procedure and blocking mechanisms for redundancy elimination. © 2010 Springer-Verlag.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    PublisherSpringer Nature
    Pages459-473
    Number of pages14
    Volume6397
    ISBN (Print)364216241X, 9783642162411
    DOIs
    Publication statusPublished - 2010
    Event17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17 - Yogyakarta
    Duration: 1 Jul 2010 → …

    Conference

    Conference17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17
    CityYogyakarta
    Period1/07/10 → …

    Keywords

    • automated reasoning, instantiation-based methods

    Fingerprint

    Dive into the research topics of 'Labelled unit superposition calculi for instantiation-based reasoning'. Together they form a unique fingerprint.

    Cite this