scientific article; zbMATH DE number 3275554

From MaRDI portal
Publication:5559220

zbMath0173.00205MaRDI QIDQ5559220

Dag Prawitz

Publication date: 1965


Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.



Related Items

Interpolation property for bicartesian closed categories, Simple proof of the completeness theorem for second-order classical and intuitionistic logic by reduction to first-order mono-sorted logic, MELL in the calculus of structures, Variants of the basic calculus of constructions, Stabilizing quantum disjunction, Natural deduction for intuitionistic linear logic, A note on the proof theory of the \(\lambda \Pi\)-calculus, Embedding complex decision procedures inside an interactive theorem prover., Hypersequents, logical consequence and intermediate logics for concurrency, A constructive valuation semantics for classical logic, Strong normalization from weak normalization in typed \(\lambda\)-calculi, A strong normalization result for classical logic, Natural deduction based upon strict implication for normal modal logics, On the semantics of the universal quantifier, Discrete tense logic with infinitary inference rules and systematic frame constants: A Hilbert-style axiomatization, A reduction rule for Peirce formula, Program tactics and logic tactics, Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels, Fibred semantics for feature-based grammar logic, Structured proof procedures, A first order logic of effects, Some general results about proof normalization, Experiments in linear natural deduction, Distributed first order logic, On the equivalence conjecture for proof-theoretic harmony, A more general general proof theory, On the strong normalisation of intuitionistic natural deduction with permutation-conversions, Reprint of: ``A more general general proof theory, Bilateralism does not provide a proof theoretic treatment of classical logic (for technical reasons), Abstract argumentation systems, A semantic framework for proof evidence, Anything goes, Sequent calculus for classical logic probabilized, Reasoning processes in propositional logic, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, Maehara-style modal nested calculi, Knowledge-based proof planning, On argumentation logic and propositional logic, Gödel's natural deduction, Normalization of N-graphs via sub-N-graphs, Fibrational modal type theory, The polarized \(\lambda\)-calculus, Classical natural deduction for S4 modal logic, Principal types of BCK-lambda-terms, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, Subatomic natural deduction for a naturalistic first-order language with non-primitive identity, Non-strictly positive fixed points for classical natural deduction, On the idea of a general proof theory, Natural deduction for first-order hybrid logic, A note on the elimination rules, On some intuitionistic modal logics, Cut-elimination theorem for relevant logics, Subatomic negation, What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics, Atomic polymorphism and the existence property, A study of Kripke-type models for some modal logics by Gentzen's sequential method, On analysing relevance constructively, Intuitionistic propositional logic is polynomial-space complete, The typed lambda-calculus is not elementary recursive, Partial logics reconsidered: A conservative approach, Hopeful monsters: a note on multiple conclusions, The complexity of Gentzen systems for propositional logic, An epistemic approach to paraconsistency: a logic of evidence and truth, Classical harmony and separability, Structured calculational proof, Certifying proofs for SAT-based model checking, The calculus of natural calculation, Infiniteness of \(\text{proof}(\alpha)\) is polynomial-space complete, Permutability of proofs in intuitionistic sequent calculi, Termination of permutative conversions in intuitionistic Gentzen calculi, Key notions of Tarski's methodology of deductive systems, Craig's interpolation theorem for the intuitionistic logic and its extensions - a semantical approach, The foundation of a generic theorem prover, Extraction and verification of programs by analysis of formal proofs, Human-centered automated proof search, Harmony and autonomy in classical logic, A Gentzen-style sequent calculus of constructions with expansion rules, On the intuitionistic force of classical search, Correspondences between classical, intuitionistic and uniform provability, Proof-search in type-theoretic languages: An introduction, Single-assumption systems in proof-theoretic semantics, Game of grounds, The category of finite sets and Cartesian closed categories, Typability and type checking in System F are equivalent and undecidable, The complexity of the disjunction and existential properties in intuitionistic logic, Structuring metatheory on inductive definitions, Conservation and uniform normalization in lambda calculi with erasing reductions, Proof methods for reasoning about possibility and necessity, The inevitability of inconsistent abstract spaces, Implementing tactics and tacticals in a higher-order logic programming language, Multilanguage hierarchical logics, or: How we can do without modal logics, Set-theoretical and other elementary models of the \(\lambda\)-calculus, Defining concurrent processes constructively, Full intuitionistic linear logic, Church-Rosser property of a simple reduction for full first-order classical natural deduction, Authentication tests and the structure of bundles., Combining type disciplines, Peirce's rule in natural deduction., Varieties of linear calculi, \(QPC_ 2\): A constructive calculus with parameterized specifications, LF+ in Coq for "fast and loose" reasoning, THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS), From petri nets to linear logic, Intuitive counterexamples for constructive fallacies, RIGOUR AND PROOF, Negative predication and distinctness, Identity and harmony and modality, On feasible numbers, The placeholder view of assumptions and the Curry-Howard correspondence, An ecumenical notion of entailment, When programs have to watch paint dry, A dialogical route to logical pluralism, Combinatorial flows as bicolored atomic flows, RELEVANCE FOR THE CLASSICAL LOGICIAN, Varieties of Relevant S5, Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts, Proof Compression and NP Versus PSPACE II: Addendum, Stateful Realizers for Nonstandard Analysis, Adding Negation to Lambda Mu, Logical multilateralism, TRANSLATIONS BETWEEN LINEAR AND TREE NATURAL DEDUCTION SYSTEMS FOR RELEVANT LOGICS, The elimination of maximum cuts in linear logic and BCK logic, A Sequent Systems without Improper Derivations, Linearity and uniqueness: an entente cordiale, UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC, Natural deduction calculi for classical and intuitionistic S5, WHAT IS A RULE OF INFERENCE?, A Classification of Improper Inference Rules, Structural Rules in Natural Deduction with Alternatives, Core Type Theory, On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\), Bilateral Rules as Complex Rules, Harmony and Normalisation in Bilateral Logic, A negative solution to Ono's problem P52: existence and disjunction properties in intermediate predicate logics, Deductive Completeness, Unnamed Item, Proof Compression and NP Versus PSPACE II, BOLZANO’S CONCEPT OF GROUNDING (ABFOLGE) AGAINST THE BACKGROUND OF NORMAL PROOFS, Proof Terms for Generalized Natural Deduction, Interpreting descriptions in intensional type theory, Peirce's Rule in a Full Natural Deduction System, WEAK DISHARMONY: SOME LESSONS FOR PROOF-THEORETIC SEMANTICS, Local Models Semantics, or contextual reasoning = locality + compatibility, E, R AND γ, Unnamed Item, A phase semantics for polarized linear logic and second order conservativity, Unnamed Item, Intrinsic reasoning about functional programs. I: First order theories, Normal forms and syntactic completeness proofs for functional independencies, On the proof theory of Coquand's calculus of constructions, The Cantor–Bernstein theorem: how many proofs?, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, A new connective in natural deduction, and its application to quantum computing, Prawitz, Proofs, and Meaning, Inferential Semantics, Cut Elimination, Substitution and Normalisation, Inversion Principles and Introduction Rules, Meaning in Use, On Constructive Fragments of Classical Logic, General-Elimination Harmony and Higher-Level Rules, Harmony in Proof-Theoretic Semantics: A Reductive Analysis, Paradox and Inconsistency: Revising Tennant’s Distinction Through Schroeder-Heister’s Assumption Rules, A Cut-Like Inference in a Framework of Explicit Composition for Various Calculi of Natural Deduction, A new connective in natural deduction, and its application to quantum computing, Unnamed Item, Normalized natural deduction systems for some relevant logics I: The logic DW, Completeness and Herbrand theorems for nominal logic, A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic: Natural Deduction and Normalisation, Proof-Theoretic Semantics and Feasibility, Relevance Logic as a Conservative Extension of Classical Logic, Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus, Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation, On the Structure of Natural Deduction Derivations for “Generally”, Type Theories from Barendregt’s Cube for Theorem Provers, Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory, An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited, Unnamed Item, Truth and Proof in Intuitionism, Constructive Modalities with Provability Smack, Emptiness and Discharge in Sequent Calculus and Natural Deduction, CUT FOR CLASSICAL CORE LOGIC, Neo-Logicism and Its Logic, Isomorphism of intersection and union types, A note on existential instantiation, CATEGORICAL HARMONY AND PATH INDUCTION, Towards a Proof Theory for Heterogeneous Logic Combining Sentences and Diagrams, A connection between cut elimination and normalization, Proof-theoretic semantics, a problem with negation and prospects for modality, Reconsidering pairs and functions as sets, Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective), An expressivist bilateral meaning-is-use analysis of classical propositional logic, Implication and analysis in classical Frege structures, Globalization of intuitionistic set theory, Models for normal intuitionistic modal logics, Models for stronger normal intuitionistic modal logics, On the syntax of Martin-Löf's type theories, Simplifying proofs in Fitch-style natural deduction systems, A weak intuitionistic propositional logic with purely constructive implication, A compact representation of proofs, Natural deduction calculi and sequent calculi for counterfactual logics, The semantics and proof theory of linear logic, On Goedel speed-up and succinctness of language representations, Proof theory for reasoning with Euler diagrams: a logic translation and normalization, The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic, General-elimination harmony and the meaning of the logical constants, Intruder deduction for the equational theory of abelian groups with distributive encryption, Natural deduction and Curry's paradox, Natural deduction and coherence for weakly distributive categories, The epistemic significance of valid inference, The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics, What does logic have to tell us about mathematical proofs?, Existential type systems between Church and Curry style (type-free style), Normalization proof for Peano arithmetic, Prolegomena to a theory of mechanized formal reasoning, A proof-theoretic universal property of determiners, From types to sets, The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof, The nature of information: a relevant approach, Implications-as-rules vs. implications-as-links: an alternative implication-left schema for the sequent calculus, Closed categories and the theory of proofs, Proof-theoretical analysis: Weak systems of functions and classes, Intuitionism and the liar paradox, A new reduction sequence for arithmetic, Primitive recursive estimate of strong normalization for predicate calculus, Preservation of equivalence of derivations under reduction of depth of formulas, Growth of length of sequential derivation transformed into natural one, Bounded memory Dolev-Yao adversaries in collaborative systems, Efficient representation of the attacker's knowledge in cryptographic protocols analysis, A globalization of the Hahn-Banach theorem, Continuations in possible-world semantics, Proof normalization with nonstandard objects, Bilateralism in proof-theoretic semantics, A logic inspired by natural language: quantifiers as subnectors, First order expressivist logic, A decision procedure revisited: Notes on direct logic, linear logic and its implementation, Harmonising natural deduction, An intuitionistic theory of types with assumptions of high-arity variables, On the adequacy of representing higher order intuitionistic logic as a pure type system, Compositional Z: confluence proofs for permutative conversion, On harmony and permuting conversions, Logical foundations for programming semantics, Existential instantiation and normalization in sequent natural deduction, Functional interpretations of feasibly constructive arithmetic, A theory of abstraction, Coquand's calculus of constructions: A mathematical foundation for a proof development system, Theo: An interactive proof development system, Partial inductive definitions as type-systems for \(\lambda\)-terms, General-elimination stability, A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's \(\varepsilon\)-terms, Yet another bijection between sequent calculus and natural deduction, Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus, A generalized syllogistic inference system based on inclusion and exclusion relations, The connection between two ways of reasoning about partial functions, Natural deduction for dual-intuitionistic logic, A consistent theory of attributes in a logic without contraction, \(\mathcal {BCDL}\): Basic constructive description logic, Combining linear-time temporal logic with constructiveness and paraconsistency, A framework for proof systems, A new normalization strategy for the implicational fragment of classical propositional logic, On the form of witness terms, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Normalization and excluded middle. I, Pedagogical second-order \(\lambda \)-calculus, The \(\lambda \)-calculus and the unity of structural proof theory, Truth-value semantics and functional extensions for classical logic of partial terms based on equality, Coherence in linear predicate logic, Method of invariant transformations and logical deduction, Wythoff games, continued fractions, cedar trees and Fibonacci searches, Normal derivations and sequent derivations, A modal logic internalizing normal proofs, Proof theory of Nelson's paraconsistent logic: a uniform perspective, CPS-translation as adjoint, Strong normalization property for second order linear logic, Correctness of programs with Pascal-like procedures without global variables, Principal type schemes for an extended type theory, To be and not to be: Dialectical tense logic, Completeness of type assignment in continuous lambda models, The completeness of intuitionistic logic with respect to a validity concept based on an inversion principle, On sequence-conclusion natural deduction systems, The structure of free closed categories, Extraction of redundancy-free programs from constructive natural deduction proofs, Simple consequence relations, Proof theory for linear lattices, Comparing formal theories of context in AI, Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere, Foundation of logic programming based on inductive definition, Formal metatheory of the lambda calculus using Stoughton's substitution, Variants of Gödel's ontological proof in a natural deduction calculus, NORMAL DERIVABILITY IN CLASSICAL NATURAL DEDUCTION, Rudimentary Kripke models for the intuitionistic propositional calculus, A normal form for logical derivations implying one for arithmetic derivations, A simple sequent calculus for partial functions, Is cut-free logic fit for unrestricted abstraction?, Back from the future, Label-free natural deduction systems for intuitionistic and classical modal logics, General proof theory: introduction, The fundamental problem of general proof theory, Gödel on deduction, Proof compression and NP versus PSPACE, Logicality, double-line rules, and modalities, Postponement of $\mathsf {raa}$ and Glivenko's theorem, revisited, Is there a ``Hilbert thesis?, The naturality of natural deduction, Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics, Terminating calculi and countermodels for constructive modal logics, Game semantics for constructive modal logic, Calculi of epistemic grounding based on Prawitz's theory of grounds, Antirealism, Meaning and Truth-Conditional Semantics, A higher-order calculus and theory abstraction, Inductive types and type constraints in the second-order lambda calculus, Uniform proofs as a foundation for logic programming, Gentzen's Proof Systems: Byproducts in a Work of Genius, A modal view on resource-bounded propositional logics, A canonical locally named representation of binding, A branching distributed temporal logic for reasoning about entanglement-free quantum state transformations, Economic reasoning with demand and supply graphs, Revisiting Quine on truth by convention, Essential structure of proofs as a measure of complexity, A refined interpretation of intuitionistic logic by means of atomic polymorphism, A metatheory of a mechanized object theory, Empty logics, Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications, What is the logic of inference?, The original sin of proof-theoretic semantics, Proof-theoretic harmony: towards an intensional account, The placeholder view of assumptions and the Curry-Howard correspondence (extended abstract), Book review of: N. Kürbis, Proof and falsity: a logical investigation, First-order automated reasoning with theories: when deduction modulo theory meets practice, Formulating deflationism, Composition of deductions within the propositions-as-types paradigm, Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes, Domain-Freeλµ-Calculus, 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000, Natural deduction bottom up, A proof-theoretic foundation of abortive continuations, Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization, Full classical S5 in natural deduction with weak normalization, A Brief History of Natural Deduction, Harmony in multiple-conclusion natural-deduction, A co-free construction for elementary doctrines, Hybrid-logical reasoning in the Smarties and Sally-Anne tasks, Gentzen and Jaśkowski natural deduction: fundamentally similar but importantly different, Normal proofs, cut free derivations and structural rules, The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony, Hypersequent and display calculi -- a unified perspective, Conditionals in reasoning, Radical anti-realism, Wittgenstein and the length of proofs, Comments on predicative logic, Logic as instrument: the millian view on the role of logic, Computing interpolants in implicational logics, Translations between Gentzen-Prawitz and Jaśkowski-Fitch natural deduction proofs, Variations on a theme of Curry, A general method for proving decidability of intuitionistic modal logics, Intuitionistic hybrid logic, The harmony of identity, GENERALITY AND EXISTENCE: QUANTIFICATIONAL LOGIC IN HISTORICAL PERSPECTIVE, The justification of identity elimination in Martin-Löf's type theory, Proof, meaning and paradox: some remarks, On paradoxes in normal form, Natural deduction for modal logic with a backtracking operator, Somehow things do not relate: on the interpretation of polyadic second-order logic, Inductive Completeness of Logics of Programs, How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning, Using well-founded relations for proving operational termination, A Curry–Howard View of Basic Justification Logic, Normality, non-contamination and logical depth in classical natural deduction, Learning Inference by Induction, Vollständigkeit und Schnittelimination in der intuitionistischen Typenlogik, Deduction normalization theorem for Sette's logic and its modifications, Ein syntaktischer Beweis für die Zulässigkeit der Schnittregel im Kalkül von Schütte für die intuitionistische Typenlogik, Ein starker Normalisationssatz für die intuitionistische Typentheorie, On maximal intermediate predicate constructive logics, A simple proof of second-order strong normalization with permutative conversions, Maximum segments as natural deduction images of some cuts, Steps towards a proof-theoretical semantics, Proof-theoretic semantics, self-contradiction, and the format of deductive reasoning, Order-enriched categorical models of the classical sequent calculus, An Infinitary System for the Least Fixed-Point Logic restricted to Finite Models, On the Convergence of Reduction-based and Model-based Methods in Proof Theory, Deduction Graphs with Universal Quantification, Did Aristotle endorse Aristotle's thesis? A case study in Aristotle's metalogic, A logical foundation of arithmetic, An alternative normalization of the implicative fragment of classical logic, Idempotent variations on the theme of exclusive disjunction, Normalisation and subformula property for a system of classical logic with Tarski's rule, The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives, Proof Theory in Philosophy of Mathematics, Automatically Proving and Disproving Feasibility Conditions, Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics, Proofs as Objects, Proof-Search in Natural Deduction Calculus for Classical Propositional Logic, Implementing Cantor’s Paradise, THE RELEVANCE OF PREMISES TO CONCLUSIONS OF CORE PROOFS, A History of Until, The Rule of Existential Generalisation and Explicit Substitution, Unnamed Item, CUT FOR CORE LOGIC, HARMONISING HARMONY, Structuring metatheory on inductive definitions, Remarks on the Church-Rosser Property, Annual Meeting of the Association for Symbolic Logic, Pittsburgh, 1991, A multicontext architecture for formalizing complex reasoning, Annual meeting of the Association for Symbolic Logic, Notre Dame, 1993, BILATERAL RELEVANT LOGIC, Type inference in polymorphic type discipline, Parametricity of extensionally collapsed term models of polymorphism and their categorical properties, Intersection and union types, Greek Geometrical Analysis, A LOGICAL ANALYSIS OF RULE INCONSISTENCY, Extending the Curry-Howard interpretation to linear, relevant and other resource logics, Gentzen's Proof of Normalization for Natural Deduction, AUTOMATED CORRESPONDENCE ANALYSIS FOR THE BINARY EXTENSIONS OF THE LOGIC OF PARADOX, Sequent calculus in natural deduction style, Equivalences between logics and their representing type theories, On Inversion Principles, Some Weak Variants of the Existence and Disjunction Properties in Intermediate Predicate Logics, Unnamed Item, Unnamed Item, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, Stanisław Jaśkowski and Natural Deduction Systems, Pragmatic and dialogic interpretations of bi-intuitionism. Part I, Unnamed Item, A Critical Overview of the Most Recent Logics of Grounding, Circumscription within monotonic inferences, Ideal and real belief about belief, Which Quantifiers Are Logical? A Combined Semantical and Inferential Criterion, Implicit Definitions, Second-Order Quantifiers, and the Robustness of the Logical Operators, THE SUBFORMULA PROPERTY IN CLASSICAL NATURAL DEDUCTION ESTABLISHED CONSTRUCTIVELY, Manipulating Sources of Information: Towards an Interpretation of Linear Logic and Strong Relevance Logic, Natural Deduction Systems for Logics in the FDE Family, The Concepts of Proof and Ground, Inferential Semantics, Paraconsistency, and Preservation of Evidence, GP’s LP, A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION, Classical Call-by-Need and Duality, 1996–97 Annual Meeting of the Association for Symbolic Logic, On the intuitionistic force of classical search (Extended abstract), A natural deduction approach to dynamic logic, The PRIZ system and propositional calculus, A short proof of the strong normalization of classical natural deduction with disjunction, Proof normalization modulo, Locally cartesian closed categories and type theory, SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS, A filter lambda model and the completeness of type assignment, 2003 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquim '03, A sequent calculus for type assignment, Unnamed Item, Commentary and Illocutionary Expressions in Linear Calculi of Natural Deduction, A Labeled Natural Deduction System for a Fragment of CTL *, Eine Funktionalinterpretation der prädikativen Analysis, Plugging-in proof development environments usingLocksinLF, ON THE SYNTAX OF LOGIC AND SET THEORY, Unnamed Item, 2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium '02, 2004 Summer Meeting of the Association for Symbolic Logic, PRESERVATION OF STRUCTURAL PROPERTIES IN INTUITIONISTIC EXTENSIONS OF AN INFERENCE RELATION, First steps in intuitionistic model theory, Choice sequences and reduction processes, Existential Type Systems with No Types in Terms, Implementing a normalizer using sized heterogeneous types, RULES FOR SUBATOMIC DERIVATION, Truth-values as labels: a general recipe for labelled deduction, Social processes, program verification and all that, INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES, Das Problem der apagogischen Beweise in BolzanosBeyträgenund seinerWissenschaftslehre, Aristotle's Syllogistic and Core Logic, Natural deduction systems for Nelson's paraconsistent logic and its neighbors, Why does the proof-theory of hybrid logic work so well?, Mereotopology in 2nd-Order and Modal Extensions of Intuitionistic Propositional Logic, Full Lambek Calculus in natural deduction, A first approach to abstract modal logics, NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF, Does the Implication Elimination Rule Need a Minor Premise?, Incorrect Responses in First-Order False-Belief Tests: A Hybrid-Logical Formalization, Definite Descriptions in Intuitionist Positive Free Logic, Normalisation for Some Quite Interesting Many-Valued Logics, European Summer Meeting of the Association for Symbolic Logic, Uppsala 1991, Popper's theory of deductive inference and the concept of a logical constant, 1999–2000 Winter Meeting of the Association for Symbolic Logic, CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI, Probabilized Sequent Calculus and Natural Deduction System for Classical Logic, Toward useful type-free theories. I, A natural extension of natural deduction, Comments on the Contributions, THE ELIMINATION OF ATOMIC CUTS AND THE SEMISHORTENING PROPERTY FOR GENTZEN’S SEQUENT CALCULUS WITH EQUALITY, Equivalence between semantics for intuitionism. I