Natural deduction for bi-intuitionistic logic

Journal of Applied Logic - Tập 25 - Trang S72-S96 - 2017
Luca Tranchini1
1Computer Science Department, Eberhard Karls Universität Tübingen, Germany

Tài liệu tham khảo

Bellin Buisman, 2007, A cut-free sequent calculus for bi-intuitionistic logic Crolard, 2001, Subtractive logic, Theor. Comput. Sci., 254, 151, 10.1016/S0304-3975(99)00124-3 Crolard, 2004, A formulae-as-types interpretation of subtractive logic, J. Log. Comput., 14, 529, 10.1093/logcom/14.4.529 de Oliveira, 2001 Dragalin, 1988 Girard, 1987, Linear logic, Theor. Comput. Sci., 56, 1, 10.1016/0304-3975(87)90045-4 Goodman, 1981, The logic of contradiction, Z. Math. Log. Grundl. Math., 27, 119, 10.1002/malq.19810270803 Goré, 2000, Dual intuitionistic logic revisited Goré, 2008, Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents, 43 Humberstone, 2005, Contrariety and subcontrariety: the anatomy of negation (with special reference to an example of J.-Y. Béziau), Theoria, 71, 241, 10.1111/j.1755-2567.2005.tb00886.x McKinsey, 1939, Proof of the independence of the primitive symbols of Heyting's calculus of propositions, J. Symb. Log., 4, 155, 10.2307/2268715 Milne, 1994, Classical harmony: rules of inference and the meaning of the logical constants, Synthese, 100, 49, 10.1007/BF01063921 Pinto, 2009, Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents, vol. 5607, 295 Pinto, 2011, Relating sequent calculi for bi-intuitionistic propositional logic, vol. 47, 57 Prawitz, 1971, Ideas and results in proof theory, vol. 63, 235 Quispe-Cruz, 2014, Intuitionistic N-graphs, Log. J. IGPL, 22, 274, 10.1093/jigpal/jzt033 Rauszer, 1974, A formalization of the propositional calculus of H-B logic, Stud. Log., 33, 23, 10.1007/BF02120864 Rauszer, 1974, Semi-boolean algebras and their applications to intuitionistic logic with dual operations, Fundam. Math., 83, 219, 10.4064/fm-83-3-219-249 Rauszer, 1977, Applications of kripke models to Heyting–Brouwer logic, Stud. Log., 36, 61, 10.1007/BF02121115 Restall Restall, 2014, Normal proofs, cut free derivations and structural rules, Stud. Log., 102, 1143, 10.1007/s11225-014-9598-4 Schroeder-Heister, 2009, Schluß und Umkehrschluß: ein Beitrag zur Definitionstheorie, vol. 3 Shoesmith, 1978 Tranchini, 2010, Refutation: a proof-theoretic account Tranchini, 2012, Natural deduction for dual-intuitionistic logic, Stud. Log., 100, 631, 10.1007/s11225-012-9417-8 L. Tranchini, G. Bellin, n.d., A refutation calculus for intuitionistic logic, Under review. Troelstra, 1996 Ungar, 1992, Normalization, Cut-Elimination, and the Theory of Proofs Urbas, 1996, Dual-intuitionistic logic, Notre Dame J. Form. Log., 37, 440, 10.1305/ndjfl/1039886520 Wansing, 2008, Constructive negation, implication, and co-implication, J. Appl. Non-Class. Log., 18, 341, 10.3166/jancl.18.341-364 Wansing, 2013, Falsification, natural deduction and bi-intuitionistic logic, J. Log. Comput., 26, 425, 10.1093/logcom/ext035 Wansing, 2017, A more general general proof theory, J. Appl. Log., 25, 23, 10.1016/j.jal.2017.01.002 Wolter, 1998, On logics with coimplication, J. Philos. Log., 27, 353, 10.1023/A:1004218110879