Refutation systems are axiomatic systems applied to non-valid formulas (or sequents). A refutation system consists of refutation axioms and refutation rules. We say that a formula A is refutable iff A is derivable from refutation axioms by refutation rules (or, dually, A multiple-conclusion entails some refutation axioms). The concept was introduced by Łukasiewcz, but the idea of refutation was already known to Aristotle. This approach is complementary to standard proof methods. Although refutation systems are not widely known, we believe that the method has potential and can produce results that are both interesting and useful.

The first Refutation Symposium took place 14-15 September in Poznan, Poland. The goal of this conference was to explain key concepts and techniques, and present new results on refutation systems. It was a place where refutation researchers from various areas of logic met to discuss their results.

The list of participants together with the slides of their talks (where available) is as follows.

Tomasz Skura
, *Refutations in logics related to Johansson’s, Nelson’s, and Segerberg’s* [pdf]

Valentin Goranko, *Proofs and refutations getting married* [pdf]

Adam Trybus, *Implementing refutation calculi: a case study*

Heinrich Wansing, *Refutation as falsification* [pdf]

Gabriele Pulcini, *From complementary logic to proof-theoretic semantics* [pdf]

Camillo Fiorentini, *Applying the inverse method to refutation calculi* [pdf]

Hans Tompits, *From Łukasiewicz to Gentzen: On sequent-type refutation calculi for three-valued logics* [pdf]

Luca Tranchini and Gianluigi Bellin, *A refutation calculus for Intuitionistic Logic *[pdf]