Baaz, Matthias and Ciabattoni, Agata and Fermüller, Christian G - Theorem proving for prenex G\"odel logic with Delta: checking validity and unsatisfiability

lmcs:833 - Logical Methods in Computer Science, March 6, 2012, Volume 8, Issue 1
Theorem proving for prenex G\"odel logic with Delta: checking validity and unsatisfiability

Authors: Baaz, Matthias and Ciabattoni, Agata and Fermüller, Christian G

G\"odel 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.


Source : oai:arXiv.org:1202.6352
DOI : 10.2168/LMCS-8(1:20)2012
Volume: Volume 8, Issue 1
Published on: March 6, 2012
Submitted on: February 1, 2011
Keywords: Computer Science - Logic in Computer Science,F.4.1


Share

Consultation statistics

This page has been seen 62 times.
This article's PDF has been downloaded 17 times.