On the Deduction Problem in Godel and Product Logics

摘要

We investigate the deduction problem in Godel and Product logics, both equipped with Godel negation, in the countable case. Our approach is based on translation of a formula to an equivalent satisfiable finite order clausal theory, consisting of order clauses. An order clause is a finite set of order literals of the form ε_1◇ ε_2 where o is a connective either = or ＜. = and ＜ are interpreted by th xe equality and standard strict linear order on, respectively. We generalise the well-known hyperresolution principle to the standard first-order Goedel logic and devise a calculus operating over order clausal theories. A variant of the DPLL procedure in the prepositional Product logic exploiting trichotomy and operating over order clausal theories, will be proposed. Both the calculi are refutation sound and complete for the countable case.