Seminár z teoretickej informatiky - Dušan Guller (20.11.2015)

v piatok 20.11.2015 o 11:00 hod. v miestnosti M/213

---

Prednášajúci:  doc. RNDr. Dušan Guller, PhD.

Názov: An Order Hyperresolution Calculus for Gödel Logic with Truth Constants and Equality, Strict Order, Delta

Termín: 20.11.2015, 11:00 hod., M/213

Abstrakt:
We present a hyperresolution calculus suitable for automated deduction in a useful   expansion of Gödel logic by intermediate truth constants and the equality, strict order, projection - Delta operators. We solve the deduction problem of a formula from a countable theory in this expansion. Gödel logic is augmented by a countable set of intermediate truth constants bar{c}, c in (0,1). Our approach is based on translation of a formula to an equivalent satisfiable finite order clausal theory, consisting of order clauses. We shall investigate the so-called canonical standard completeness, where the semantics of Gödel 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 the investigated expansion of Gödel logic.

---