[Back]

J. Oetsch, H. Tompits:
"Gentzen-type Refutation Systems for Three-Valued Logics";
Talk: 24th Workshop on (Constraint) Logic Programming (WLP 2010), Kairo; 09-14-2010 - 09-16-2010; in: "24th Workshop on (Constraint) Logic Programming WLP'2010", S. Abdennadher (ed.); Technical Report, Faculty of Media Engineering and Technology, German University in Cairo, Kario, Ägypten (2010), 88 - 98.

While the purpose of a conventional proof calculus is to axiomatise the set of valid sentences of a given logic, a refutation system, or complementary calculus, is concerned with axiomatising the invalid sentences. Instead of exhaustively searching for counter models for some sentence, refutation systems establish invalidity by deduction and thus in a purely syntactic way. Such systems are relevant not only for proof-theoretic reasons but also for realising deductive systems for nonmonotonic logics. In this paper, we introduce Gentzen-type refutation systems for two basic three-valued logics that allow to embed well-known three-valued logics relevant for AI and logic programming like that of Kleene, Lukasiewicz, Gödel, as well as three-valued paraconsistent logics. As an application of our calculus, we provide derived rules for Gödel's three-valued logic, allowing to decide strong equivalence of logic programs under the answer-set semantics.

automated deduction, refutation calculus, answer set programming

http://publik.tuwien.ac.at/files/PubDat_187985.pdf

Project Head Hans Tompits:
Softwareentwicklung in der Answer-Set Programmierung