A general theory of refutation systems is given. Some applications (concerning maximality and minimality in lattices of logics) are also discussed.

In the paper we study the method of Socratic proofs in the intuitionistic propositional logic as a reduction procedure. Our approach consists in constructing for a given sequent α a finite tree of sets of sequents by using invertible reduction rules of the kind: ? is valid if and only if ?1 is valid or... or ?n is valid. From such a tree either a Gentzen-style proof of α or an Aristotle-style refutation of α can also be extracted.

In this paper we study the method of refutation rules in the modal logic K4. We introduce refutation rules with certain normal forms that provide a new syntactic decision procedure for this logic. As corollaries we obtain such results for the following important extensions: S4, the provability logic G, and Grzegorczyk''s logic. We also show that tree-type models can be constructed from syntactic refutations of this kind.

In this paper we study the method of refutation rules in the modal logic K4. We introduce refutation rules with certain normal forms that provide a new syntactic decision procedure for this logic. As corollaries we obtain such results for the following important extensions: S4, the provability logic G, and Grzegorczyk's logic. We also show that tree-type models can be constructed from syntactic refutations of this kind.

The purpose of the paper is to study syntactic refutation systems as a way of characterizing normal modal propositional logics. In particular it is shown that there is a decidable modal logic without the finite model property that has a simple finite refutation system.

The goal of this paper is to generalize specific techniques connected with refutation rules involving certain normal forms. In particular, a method of axiomatizing both a logic L and its complement −L is introduced.

In Section 2 I give a criterion of decidability that can be applied to logics (i.e. Tarski consequence operators) without the finite model property. In Section 3 I study ukasiewicz-style refutation procedures as a method of obtaining decidability results.This method also proves to be more general than Harrop's criterion.

A sufficient condition for an extension of positive logic with strong negation to be characterized by a class of finite trees is given.

The goal of this paper is to analyse Implicational Relevance Logic from the point of view of refutability. We also correct an inaccuracy in our paper “The RM paraconsistent refutation system”.

The purpose of the paper is to make a few remarks on the following aspects of refutation rules: a characteristic property of a logic, elegant and constructive completeness proofs. In particular a new constructive completeness proof for the provability logic G is given.

The aim of this paper is to study the refutation system consisting of the refutation axiom p ∧ ¬p → q and the refutation rules: reverse substitution and reverse modus ponens (B/A, if A → B ∈ RM). It is shown that the refutation system is characteristic for the logic of the 3-element RM algebra.

This volume contains papers presented at the Poznań Reasoning Week multi-conference held in Poznań in September 11-15, 2018. PRW aims at bringing together experts whose research offers a broad range of perspectives on systematic analyses of reasoning processes and their formal modelling. The 2018 edition consisted of three conferences, which addressed the following topics: (i) games in reasoning research, (ii) the interplay of logic and cognition, and (iii) refutation systems. The papers collected in this volume address all these topics.