Blocking and other enhancements for bottom-up model generation methods

Peter Baumgartner, Renate A. Schmidt

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

    Abstract

    In this paper we introduce several new improvements to the bottom-up model generation (BUMG) paradigm. Our techniques are based on non-trivial transformations of first-order problems into a certain implicational form, namely range-restricted clauses. These refine existing transformations to range-restricted form by extending the domain of interpretation with new Skolem terms in a more careful and deliberate way. Our transformations also extend BUMG with a blocking technique for detecting recurrence in models. Blocking is based on a conceptually rather simple encoding together with standard equality theorem proving and redundancy elimination techniques. This provides a general-purpose method for finding small models, The presented techniques are implemented and have been successfully tested with existing theorem provers on the satisfiable problems from the TPTP library. © Springer-Verlag Berlin Heidelberg 2006.
    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.
    Pages125-139
    Number of pages14
    Volume4130
    Publication statusPublished - 2006
    EventThird International Joint Conference on Automated Reasoning, IJCAR 2006 - Seattle, WA
    Duration: 1 Jul 2006 → …

    Conference

    ConferenceThird International Joint Conference on Automated Reasoning, IJCAR 2006
    CitySeattle, WA
    Period1/07/06 → …

    Fingerprint

    Dive into the research topics of 'Blocking and other enhancements for bottom-up model generation methods'. Together they form a unique fingerprint.

    Cite this