scientific article; zbMATH DE number 3358455
From MaRDI portal
zbMath0226.02031MaRDI QIDQ5632554
Publication date: 1971
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
A connection between cut elimination and normalization, On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem, Syntactic analysis of \(\eta\)-expansions in pure type systems., Generality of proofs and its Brauerian representation, Is cut-free logic fit for unrestricted abstraction?, Stabilizing quantum disjunction, Natural deduction for intuitionistic linear logic, The fundamental problem of general proof theory, The naturality of natural deduction, Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics, Calculi of epistemic grounding based on Prawitz's theory of grounds, Algebraic proofs of cut elimination, Combinatory logic with polymorphic types, A Realizability Interpretation for Intersection and Union Types, Categorial generalization of algebraic recursion theory, Unnamed Item, Proof theory for reasoning with Euler diagrams: a logic translation and normalization, Economic reasoning with demand and supply graphs, A reduction rule for Peirce formula, Natural deduction and Curry's paradox, Embedding of a free cartesian-closed category into the category of sets, A formalization of Sambins's normalization for GL, ``Inference versus consequence revisited: inference, consequence, conditional, implication, Mechanizing structural induction. II: Strategies, What does logic have to tell us about mathematical proofs?, Arguments, Proofs, and Dialogues, A refined interpretation of intuitionistic logic by means of atomic polymorphism, A more general general proof theory, Reprint of: ``A more general general proof theory, Natural deduction for bi-intuitionistic logic, Abstract argumentation systems, The original sin of proof-theoretic semantics, A proof-theoretic investigation of a logic of positions, Proof-theoretic harmony: towards an intensional account, A rationale for conditional equational programming, Unnamed Item, A note on harmony, A coherence theorem for canonical morphisms in Cartesian closed categories, Partial inductive definitions, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, Domain-Freeλµ-Calculus, Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization, Proof-theoretic semantics and inquisitive logic, On the concurrent computational content of intermediate logics, On Dummett's verificationist justification procedure, Existential instantiation and normalization in sequent natural deduction, Theo: An interactive proof development system, Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms, Harmony in multiple-conclusion natural-deduction, Natural deduction for dual-intuitionistic logic, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, Hybrid-logical reasoning in the Smarties and Sally-Anne tasks, Why conclusions should remain single, 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, On the proof-theoretic foundation of general definition theory, Prelogic of logoi, Epistemic and intuitionistic formal systems, Normalization and excluded middle. I, Quantifier-complete categories, Intuitionistic hybrid logic, The harmony of identity, A note on the elimination rules, What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics, The justification of identity elimination in Martin-Löf's type theory, Proof, meaning and paradox: some remarks, On paradoxes in normal form, Failure of completeness in proof-theoretic semantics, Somehow things do not relate: on the interpretation of polyadic second-order logic, A study of Kripke-type models for some modal logics by Gentzen's sequential method, Proof nets of PN as graphs, Theory of proofs (arithmetic and analysis), Choice sequences and reduction processes, The calculus of natural calculation, Typing and computational properties of lambda expressions, Representing scope in intuitionistic deductions, Intensionality in mathematics, Normal derivations and sequent derivations, The foundation of a generic theorem prover, Extraction and verification of programs by analysis of formal proofs, Ein starker Normalisationssatz für die intuitionistische Typentheorie, Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions, Geometry and generality in Frege's philosophy of arithmetic., A simple proof of second-order strong normalization with permutative conversions, A proof description language and its reduction system, Steps towards a proof-theoretical semantics, On sequence-conclusion natural deduction systems, The inevitability of inconsistent abstract spaces, Implementing tactics and tacticals in a higher-order logic programming language, Combinatory reduction systems: Introduction and survey, Set-theoretical and other elementary models of the \(\lambda\)-calculus, Church-Rosser property of a simple reduction for full first-order classical natural deduction, Simple consequence relations, Set theory for verification. I: From foundations to functions, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction, Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere, Denotational semantics for languages of epistemic grounding based on Prawitz's theory of grounds, The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives, Extended term rewriting systems, Some lambda calculi with categorical sums and products, Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract), Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics, Unnamed Item, AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ, SUBATOMIC INFERENCES: AN INFERENTIALIST SEMANTICS FOR ATOMICS, PREDICATES, AND NAMES, Intrinsic theories and computational complexity, Choice and independence of premise rules in intuitionistic set theory, An intuitionistic formula hierarchy based on high‐school identities, The formal verification of the ctm approach to forcing, Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules, Valuative Lattices and Spectra, WHAT IS A RULE OF INFERENCE?, Bilateral Rules as Complex Rules, A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object, Théories géométriques pour l’algèbre des nombres réels, POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE, Two different strong normalization proofs?, Peirce's Rule in a Full Natural Deduction System, REPRESENTING CONJUNCTIVE DEDUCTIONS BY DISJUNCTIVE DEDUCTIONS, Intrinsic reasoning about functional programs. I: First order theories, The Cantor–Bernstein theorem: how many proofs?, Prawitz, Proofs, and Meaning, Explaining Deductive Inference, Inferential Semantics, Cut Elimination, Substitution and Normalisation, Inversion Principles and Introduction Rules, Meaning in Use, Hypothesis-Discharging Rules in Atomic Bases, Harmony in Proof-Theoretic Semantics: A Reductive Analysis, Rule-Following and the Limits of Formalization: Wittgenstein’s Considerations Through the Lens of Logic, Constructibility and Geometry, Unnamed Item, Deriving Natural Deduction Rules from Truth Tables, The normalization theorem for extended natural deduction, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus, An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited, Formal explanations as logical derivations, Neo-Logicism and Its Logic