Unsatisfiable Formulae of Gödel Logic with Truth Constants and \varDelta Are Recursively Enumerable
This paper brings a solution to the open problem of recursive enumerability of unsatisfiable formulae in the first-order Godel logic. The answer is affirmative even for a useful expansion by intermediate truth constants and the projection operator Open image in new window . The affirmative result for unsatisfiable prenex formulae of \(G_\infty ^\varDelta \) has been stated in [1]. In [2], we have generalised the well-known hyperresolution principle to the first-order Godel logic for the general case. We now propose a modification of the hyperresolution calculus suitable for automated deduction with explicit partial truth.