English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In (Guller, 2014), we have generalised the well-known hyperresolution principle to the first-order Godel logic with truth constants. This paper is a continuation of our work. We propose a hyperresolution calculus suitable for automated deduction in a useful expansion of Godel logic by intermediate truth constants and the equality, =, strict order, -<; , projection, Δ, operators. We solve the deduction problem of a formula from a countable theory in this expansion. We expand Godel logic by a countable set of intermediate truth constants C̅, c ∈ (0, 1). 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 εi is an atom or a quantified atom, and 0 is the connective = or -<;. = and -<; are interpreted by the equality and standard strict linear order on [0, 1], respectively. We shall investigate the so-called canonical standard completeness, where the semantics of Godel logic is given by the standard G-algebra and truth constants are interpreted by 'themselves'. The hyperresolution calculus is refutation sound and complete for a countable order clausal theory under a certain condition for the set of truth constants occurring in the theory. As an interesting consequence, we get an affirmative solution to the open problem of recursive enumerability of unsatisfiable formulae in Godel logic with truth constants and the equality, =, strict order, -<;, projection, Δ, operators.

An Order Hyperresolution Calculus for Gödel Logic with Truth Constants