Abstract: |
This paper addresses the deduction problem of a formula from a countable theory in the first-order G\"{o}del logic from a perspective of automated deduction. Our approach is based on the translation of a formula to an equivalent satisfiable CNF one, which contains literals of the augmented form: either a or a → b or (a→b) →b or Qx c→ a or a→Qx c where a, c are atoms different from 0 (the false), 1 (the true); b is an atom different from 1; Q ∈ {∀,∃}; x is a variable occurring in c. A CNF formula is further translated to an equivalent satisfiable finite order clausal theory, which consists of order clauses - finite sets of order literals of the form: either a ≖ b or Qx c ≖ a or a ≖ Qx c or a ≺ b or Qx c ≺ a or a ≺ Qx c where a, b, c are atoms; Q ∈ {∀,∃}; x is a variable occurring in c. ≖ and ≺ are interpreted by the equality and strict linear order on [0,1], respectively. For an input theory, the proposed translation produces a so-called semantically admissible order clausal theory. An order hyperresolution calculus, operating on semantically admissible order clausal theories, is devised. The calculus is proved to be refutation sound and complete for the countable case. |