Matthias Baaz ; Agata Ciabattoni ; Christian G Fermüller - Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability

lmcs:833 - Logical Methods in Computer Science, March 6, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:20)2012
Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiabilityArticle

Authors: Matthias Baaz ORCID; Agata Ciabattoni ORCID; Christian G Fermüller

    Gödel logic with the projection operator Delta (G_Delta) is an important many-valued as well as intermediate logic. In contrast to classical logic, the validity and the satisfiability problems of G_Delta are not directly dual to each other. We nevertheless provide a uniform, computational treatment of both problems for prenex formulas by describing appropriate translations into sets of order clauses that can be subjected to chaining resolution. For validity a version of Herbrand's Theorem allows us to show the soundness of standard Skolemization. For satisfiability the translation involves a novel, extended Skolemization method.

    Comment: 23 pages, accepted for LMCS (Logical Methods in Computer Science)

    https://doi.org/10.2168/LMCS-8(1:20)2012
    Source: arXiv.org:1202.6352
    Volume: Volume 8, Issue 1
    Published on: March 6, 2012
    Imported on: February 1, 2011
    Keywords: Computer Science - Logic in Computer Science, F.4.1
    Licence: arXiv.org - Non-exclusive license to distribute
    Funding:
      Source : OpenAIRE Graph
    • Nonclassical Proofs: Theory, Applications and Tools; Code: Y 544
    • Monadic Gödel logics; Code: P 22416

    Classifications

    Mathematics Subject Classification 20201
    Sources:
    • [1] zbMATH Open.

    2 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 2939 times.
    This article's PDF has been downloaded 728 times.