|
|
VOLUME 8, ISSUE 1, PAPER 20
|
Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability
|
©Matthias Baaz, Department of Discrete Mathematics and Geometry, TU Vienna
©Agata Ciabattoni, Department of Computer Languages, TU Vienna
©Christian G. Fermüller, Department of Computer Languages, TU Vienna
|
Abstract
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.
|
Publication date: March 6, 2012
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-8(1:20)2012
Hit Counts: 966 |
 Creative Commons | |
