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
Secondary volumes: Selected Papers of the 24th International Workshop on Computer Science Logic and the 19th Annual Conference of the EACSL (CSL 2010)
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 3179 times.
This article's PDF has been downloaded 821 times.