[Back]

H. Tompits:
"From Łukasiewicz to Gentzen: On Sequent-type Refutation Calculi for Three-valued Logics";
Keynote Lecture: Refutation Symposium 2018 at Poznań Reasoning Week, Poznań, Poland; 2018-09-11 - 2018-09-15.

While traditional proof calculi deal with the axiomatisation of the set of valid sentences of a given logic, refutation calculi, also referred to as complementary calculi, are concerned with axiomatising the invalid sentences, i.e., providing means to deduce invalid sentences from already established invalid ones. Albeit already Aristotle studied fallacies (i.e., invalid arguments) in his system of syllogisms, the first modern treatment of axiomatic rejection originates with Jan Łukasiewicz [7] and his study of expressing Aristotle´s syllogistic in modern logic [8, 9] where he introduced a Hilbert-type rejection system. This was continued by his student Jerzy Słupecki [16] and subsequently extended to a theory of rejected propositions [17, 21, 2, 18, 19]. [For a description of the development of this notion, cf., e.g., the paper by Wybraniec-Skardowska [22].] Furthermore, axiomatic rejection methods where not only studied for classical logic [13, 20] but also for varieties of logics, like intuitionistic logic [10, 4, 12], modal logics [5, 14], and others [1]. In this talk, I deal with the case of three-valued logics (and many-valued logics more generally), a logical approach again famously going back to Łukasiewicz [7]. While complete and uniform rejection methods were already quite extensively studied in the literature, like, e.g., in the works by Bryll and Maduch [3] and Skura [11], here I will discuss refutation calculi for such logics from the point of view of Gentzen-type systems. Furthermore, the relevance of the discussed calculi for nonmonotonic reasoning-notably for checking strong non-equivalence of logic programs under the answer-set semantics [6]-will be pointed out.

https://poznanreasoningweek.files.wordpress.com/2018/09/prw2018abstracts1.pdf