Theorem proving for prenex G\"odel logic with Delta: checking validity and unsatisfiability

TL;DR

This paper develops a uniform computational approach for checking validity and unsatisfiability of prenex formulas in G"odel logic with Delta, using translations into order clauses and specialized Skolemization methods.

Contribution

It introduces a novel translation framework and extended Skolemization techniques for prenex G"odel logic with Delta, enabling effective validity and satisfiability checking.

Findings

Uniform translation into order clauses for validity and satisfiability

Soundness of Skolemization for validity in G"odel logic with Delta

Extended Skolemization method for satisfiability checking

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.