Welcome to our site devoted to the notion of refutation (rejection) in logic. This is a project of the researchers from the University of Zielona Góra, Poland.
Refutation in logic has many aspects. This site aims to describe the multifaceted nature of refutation research (and as such is a work in progress). The Resources tab contains (successively extended) list of articles, expository papers, online pointers, computer code etc. Click on The People tab for a list of researchers past and present dealing with various aspects of refutation. This section also contains those directly involved in the creation of this site. The Events tab lists relevant conferences, workshops, etc, including The Goranko Challenge.
Comments? Suggestions? Click on the About tab to let us know!
Valentin Goranko and Tomasz Skura, Refutation systems in the finite (Preprint) [pdf]
Valentin Goranko, Gabriele Pulcini and Tomasz Skura Refutation Systems: An Overview and Some Applications to Philosophical Logics, Knowledge, Proofs and Dynamics: The 4th Asian Workshop on Philosophical Logic,Fenrong Liu, Hiroakira Ono, Junhua Yu (editors). (Preprint) [pdf]
Tomasz Skura, Implicational Logic, Relevance and Refutability, Logic and Logical Philosophy [pdf]
This section contains references to some of the works dealing with various aspects of refutation. A summary and a list of keywords were added, whenever possible. Contact us if you feel that there are publications that we have not included and which should make it to one of the lists below.
Table of contents
contains the most recent developments.
contains classical papers in the area.
is the place to start for those new to the topic of refutation.
offers a selection of links to the websites of researchers and refutation-related events, resources etc.
This list contains research papers on refutation published in or after 2001.
- R. Caferra and N. Peltier, Accepting/Rejecting Propositions From Accepted/Rejected Propositions: A Unifying Overview, International Journal of Intelligent Systems, 23:999–1020, 2008. [pdf]
Abstract: Looking at inference as a way of transforming information so as to make it more easily usable (or interpretable) allows to consider accepted and rejected propositions as equally relevant and naturally gives a bipolar view of reasoning. The four possibilities of transforming information from accepted or rejected propositions into accepted or rejected ones are analyzed and examples illustrating them are given. This analysis is not only interesting per se but can also be useful in increasing capabilities of existing theorem provers. A unified framework based on former work by the authors is extended by incorporating the idea of theory-anti-subsumption related to Plotkin’s generalization. Working on some technical details of this framework should allow automated reasoning tools to deal with different ways of connecting accepted and rejected propositions.
- R. Gore and L. Postniece, Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic, Journal of Logic and Computation, 20(1):233–260, 2010. [pdf]
Abstract: Bi-intuitionistic logic is the union of intuitionistic and dual intuitionistic logic, and was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ‘cut-free’ sequent calculus has recently been shown to fail cut-elimination. We present a new cut-free sequent calculus for bi-intuitionistic logic, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between intuitionistic implication and dual intuitionistic exclusion, similarly to future and past modalities in tense logic. Our calculus handles this interaction using derivations and refutations as first class citizens. We employ extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of refutations, and rules which compose certain refutations and derivations to form derivations. Automated deduction using terminating backward search is also possible, although this is not our main purpose.
Keywords: Bi-intuitionistic logic, sequent calculus, refutation calculus, proof search, decision procedure.
- J. P. Goudsmit, Admissibility and Refutation. Some Characterisations of Intermediate Logics, Archive for Mathematical Logic, 53(7–8):779–808, 2014. [pdf]
Abstract: Refutation systems are formal systems for inferring the falsity of formulae. These systems can, in particular, be used to syntactically characterise logics. In this paper, we explore the close connection between refutation systems and admissible rules. We develop technical machinery to construct refutation systems, employing techniques from the study of admissible rules. Concretely, we provide a refutation system for the intermediate logics of bounded branching, known as the Gabbay–de Jongh logics. We show that this gives a characterisation of these logics in terms of their admissible rules. To illustrate the technique, we also provide a refutation system for Medvedev’s logic.
Keywords: Intermediate logic, Admissible rules, Refutation, Gabbay–de Jongh logics, Medvedev’s logic.
- T. Skura, Refutations, Proofs, and Models in the Modal Logic K4, Studia Logica 70:193–204, 2002.
- T. Skura, Rules and Refutation Rules for the Logic of Finite n-ary Trees, Journal of Logic and Computation 14:429–435, 2004.
- T. Skura, Refutation Systems in Propositional Logic, [in:] D. Gabbay and F. Guenthner (ed.), Handbook of Philosophical Logic, Volume 16, Springer 2011, 115–157.
- T. Skura, Refutation Methods in Modal Propositional Logic, Wydawnictwo Naukowe Semper, Warszawa, 2013.
- T. Skura, What is a refutation system? [in:] A. Moktefi, A. Moretti, F. Schang (ed.), Let's Be Logical, London, College Publications, 2016.
- R. Sochacki, Rejected Axioms for the Nonsense Logic and the k-valued Logic of Sobociński, Logic and Logical Philosophy, 17:321–327, 2008. [pdf]
Abstract: In this paper rejection systems for the “nonsense-logic” W and the k-valued implicational-negational sentential calculi of Sobociński are
given. Considered systems consist of computable sets of rejected axioms and only one rejection rule: the rejection version of detachment rule.
Keywords: rejected axioms, the logic W, the k-valued sentential calculi of Sobociński.
- R. Sochacki, Refutation System for a System of Nonsense Logic, Logic and Logical Philosophy, 20:233–239, 2011. [pdf]
Abstract: In the paper rejection systems for a system of nonsense-logic
are investigated. The first rejection system consists of four rejected axioms
and only one rejection rule - the rule of rejection by detachment. The
second one consists of one rejected axiom and two rejection rules: the rule
of rejection by detachment and the rule of rejection by substitution. The
aim of the paper is to present also a proof of Ł-decidability for the considered
Keywords: refutation systems, rejected axioms, Ł-decidability
- J. Oetsch and H. Tompits, Gentzen-Type Refutation Systems for Three-Valued Logics with an Application to Disproving Strong Equivalence, [in:] J. P. Delgrande and W. Faber (eds), Logic Programming and Nonmonotonic Reasoning. LPNMR 2011. Lecture Notes in Computer Science, vol 6645. Springer, Berlin, Heidelberg, 2011. [pdf]
Abstract: While the purpose of conventional proof calculi is to axiomatise the set
of valid sentences of a logic, refutation systems axiomatise the invalid sentences.
Such systems are relevant not only for proof-theoretic reasons but also for realising
deductive systems for nonmonotonic logics. We introduce Gentzen-type refutation
systems for two basic three-valued logics and we discuss an application of one of
these calculi for disproving strong equivalence between answer-set programs.
This list contains research papers on refutation published before 2001.
- X. Caicedo, A Formal System for the Non-Theorems of the Propositional Calculus, Notre Dame Journal of Formal Logic, 19, 1978. [pdf]
Abstract: In this paper we give an analogous deductive system (more concretely, a Hilbert-type system) such that the formulae deduced are exactly those that are not tautologies, the non-theorems of the propositional calculus.
- R. Dutkiewicz, The Method of Axiomatic Rejection for the Intuitionistic Propositional Logic, Studia Logica, 48(4):449–459, 1989. [pdf]
Abstract: We prove that the intuitionistic sentential calculus is Ł-decidable (decidable in the sense of Łukasiewicz), i.e. the sets of theses of Int and of rejected formulas are disjoint and their union is equal to all formulas. A formula is rejected iff it is a sentential variable or is obtained from other formulas by means of three rejection rules. One of the rules is original, the remaining two are Łukasiewicz's rejection rules: by detachement and by substitution. We extensively use the method of Beth's semantic tableaux.
- V. Goranko, Proving Unprovability in some Normal Modal Logics. Bulletin of the Section of Logic, 20(1), 1991. [pdf]
Abstract: The present communication suggests deductive systems for the operator of unprovability in some particular propositional normal modal logics. We give thus complete syntactic characterization of these logics in the sense of Lukasiewicz: for every formula φ either φ is provable or φ is unprovable (but not both). In particular, purely syntactic decision procedure is provided for the logics under considerations.
- V. Goranko, Refutation Systems in Modal Logics. Studia Logica, 53, 1994. [pdf]
Abstract: Complete deductive systems are constructed for the non-valid (refutable) formulae and sequents of some propositional modal logics. Thus, complete syntactic characterizations in the sense of Lukasiewicz are established for these logics and, in particular, purely syntactic decision procedures for them are obtained. The paper also contains some historical remarks and a general discussion on refutation systems.
- T. Hailperin, A Complete Set of Axioms for Logical Formulas Invalid in Some Finite Domains, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 7:84–96. [pdf]
- E. G. K. Lopez-Escobar, Refutability and Elementary Number Theory, Indigationes Mathematicae, 75(4):362–374, 1972. [pdf]
Abstract: It would thus appear that there is not much difference in the case of elementary number theory whether one uses for the underlying logic intuitionsm, constructible falsity or refutability. When the domain of discourse is the species of natural numbers, mathematical induction is a very powerful principle which overcomes any deficencies which may be present. Thus if one wishes to obtain a separation of the concepts of intuitionism, constructible falsity and refutability then either one has to give up mathematical induction or else consider some species other than the natural numbers. The latter would probably be more interesting.
- G. Mints, Gentzen-type Systems and Resolution Rules, Lecture Notes in Computer Science, 417:198–231, 1990. [djvu]
Abstract: The main new result of this paper is formulation and a completeness proof of the resolution-type calculi for several propositional modal logics, including S5, S4, T, K.
- S. G. Morgan, Sentential Calculus for Logical Falsehoods, Notre Dame Journal of Formal Logic, 14(3):347–353, 1973. [pdf]
Abstract: Several axiomatic systems for sentential calculus have been developed. Such systems are generally motivated by a consideration of logically true sentences of the formal language. In this paper I present a finitely axiomatized system of sentential calculus for logically false sentences.
- W. Schönfeld, Proof Search for Unprovable Formulas, [in:] B. Neumann (ed) GWAI-83. Informatik-Fachberichte, vol 76. Springer, Berlin, Heidelberg, 1983. [pdf]
Abstract: A method is developped of how to extend theorem provers in order to decide satisfiability for every formula of prefix type AE...E. The key idea is to find a certain criterion for the existence of loops in the search tree. As a byproduct a result on proof complexity is derived.
- D. Scott, Completeness Proofs for the Intuitionistic Sentential Calculus, [in:] Summaries of Talks Presented at the Summer Institute of Symbolic Logic, Cornell University 1957, second edition Princeton, 1960, 231–241.
Abstract: Several interpretations of the intuitionistic sentential logic are considered: finite distributive lattices and the Jaskowski truth tables, open sets in a topological space, and the intuitionistically acceptable notion of properties of free choices. Exactly the provable formulae are shown to be valid in the interpretations by use of refutation rules to enumerate the unprovable formulae.
- T. Skura, A Complete Syntactical Characterization of the Intuitionistic Logic, Reports on Mathematical Logic, 23:75–80, 1989.
- T. Skura, A New Criterion of Decidability for Intermediate Logics, Bulletin of the Section of Logic, 19:10–14, 1990.
- T. Skura, On Pure Refutation Formulations of Sentential Logics, Bulletin of the Section of Logic, 19:102–107, 1990.
- T. Skura, On Decision Procedures for Sentential Logics, Studia Logica, 50:173–179, 1991.
- T. Skura, Refutation Calculi for Certain Intermediate Propositional Logics, Notre Dame Journal of Formal Logic, 33:552–560, 1992.
- T. Skura, Refutation Rules for Three Modal Logics, Bulletin of the Section of Logic, 21:31–32, 1992.
- T. Skura, Some Results Concerning Refutation Procedures, Acta Universitatis Wratislaviensis. Logika, 15:83–95, 1993.
- T. Skura, Characterizing Propositional Logics by Formulas, [in:] J. Woleński (ed.), Philosophical Logic in Poland, Kluwer, 239–245, 1994.
- T. Skura, Syntactic Refutations Against Finite Models in Modal Logic, Notre Dame Journal of Formal Logic, 35:595–605, 1994.
- T. Skura, A Łukasiewicz-style Refutation System for the Modal Logic S4, Journal of Philosophical Logic, 24:573–582, 1995.
- T. Skura, Some Aspects of Refutation Rules, Reports on Mathematical Logic, 29:109–116, 1995.
- T. Skura, Refutations and proofs in S4, [in:] H. Wansing (ed.), Proof Theory of Modal Logic, Kluwer, 1996, 45–51.
- T. Skura, A Pure Refutation Calculus for the Intuitionistic Propositional Logic, Acta Universitatis Wratislaviensis. Logika, 18:123–127, 1998.
- T. Skura, Aspects of Refutation Procedures in the Intuitionistic Logic and Related Modal Systems, Wydawnictwo Uniwersytetu Wrocławskiego, Wrocław, 1999.
: The purpose of this work is to study the method of syntactic refutations in certain important non-classical propositional logics.
- J. Słupecki, On Aristotelian Syllogistic, Journal of Symbolic Logic, 17(3): 210–211, 1952. [pdf]
- J. Słupecki and G. Bryll, Proof of Ł-decidability of Lewis System S5, Studia Logica, 32:99–105, 1973. [pdf]
Abstract: This paper is concerned with Lewis system S5 in which the primitive terms are the functors of the classical implication, negation and necessity.
- W. Staszek, On Proofs of Rejection, Studia Logica, 29(1):17–23, 1971. [pdf]
Abstract: The notion of rejected proposition was introduced to logic by Jan Lukasiewicz in connection with his inquiries about Aristotle's syllogistics. Lukasiewicz distinguishes the propositions which are axiomatically rejected from the ones rejected on the ground
of "rules of rejection". Lukasiewicz was using his notion of rejected proposition when he examined systems with no quantifiers. Therefore he did not need any rules of rejection which would have concerned quantifiers. In this paper we shall take into account such rules, too.
- A. M. Tamminga, Logics of Rejection: Two Systems of Natural Deduction, Logique et Analyse, 146:169–208, 1994. [pdf]
Abstract: This paper contains two systems o f natural deduction for the rejection of non-tautologies of Classical Propositional Logic. The first system is correct and complete with respect to the body o f all non-tautologies, the second system is correct and complete with respect to the body of all contradictions. The second system is a subsystem of the first. We begin with an historical synopsis of the development of the theories of rejection for the classical logic of propositions, taking our starting-point from the theories of their 'founding father', Jan Lukasiewicz. Subsequently, the systems of natural deduction are set forth and their correctness and completeness is
showed. We shall conclude with an interesting 'Theorem of Inversion'.
- M. Tiomkin, Proving unprovability, Proceedings of the Third Annual Symposium on Logic in Computer Science, 22–26, 1988. [pdf]
Abstract: A formal proof system for unprovability in the predicate calculi is developed. This system is shown to be complete with respect to the logic of finite structures. Its applications may be extending the "negation by failure" of Prolog, preventing infinite loops in a deductive data base or Prolog, or proving formulas in a nonmonotonic (default) logic.
This list contains papers providing an overview of some aspect of refutation.
- G. Pulcini, Some Philosophical Aspects of Refutation. [pdf]
- T. Skura, Formal Refutation Systems. [pdf]
- U. Wybraniec-Skardowska, Rejection in Łukasiewicz's and Słupecki's Sense, [in:] A. Garido, U. Wybraniec-Skardowska (eds.), The Lvov-Warsaw School, Past and Present, Springer-Birkhäuser Cham, Switzerland, 575–597. [pdf]
A map showing the locations of refutation-related research and events
Adam Trybus (www)
The Goranko Challenge
During the Refutation Symposium held in Poznań in 2018, Valentin Goranko (www) issued a challenge to the refutation community offering a tanglible prize for the winner. For details see: The Goranko Challenge. Entries and inquiries can be send at the e-mail address provided in the About section.
Refutation Symposium 2018
Organised as part of Poznań Reasoning Week, the Symposium brought together researchers from various subfields of logic. The Symposium was a joint effort of The Institute of Philosophy in Zielona Góra and The Institute of Psychology in Poznań. The book of abstracts is available here.
Chair of Logic and Methodology of Science,
Institute of Philosophy,
University of Zielona Góra
71a Wojska Polskiego
Zielona Góra 65-762
e-mail inquiries: adam DOT trybus AT gmail DOT com (Adam Trybus)
Admin: adam DOT trybus AT gmail DOT com (also for general inquiries)