scientific article; zbMATH DE number 3333259
From MaRDI portal
zbMath0209.30001MaRDI QIDQ5610986
Publication date: 1969
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Collected or selected works; reprintings or translations of classics (01A75) History of mathematical logic and foundations (03-03) Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations (03-06) Collections of translated articles of miscellaneous specific interest (00B55)
Related Items
Current trends in substructural logics, Hybrid reasoning using universal attachment, On the relative merits of path dissolution and the method of analytic tableaux, An extension of the omega-rule, Kripke-completeness and cut-elimination theorems for intuitionistic paradefinite logics with and without quasi-explosion, Syntactical investigations into \(BI\) logic and \(BB^ \prime I\) logic, The enduring scandal of deduction. Is propositional logic really uninformative?, Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq, A cut elimination theorem for stationary logic, A cut-free Gentzen-type system for the logic of the weak law of excluded middle, Dual-intuitionistic logic, The linear abstract machine, Between Hilbert and Gentzen: four-valued consequence systems and structural reasoning, The semantics and proof theory of linear logic, Consequence and confirmation, A note on sequent calculi intermediate between LJ and LK, Productive use of failure in inductive proof, An answer to an open problem of Urquhart, Semantics and proof-theory of depth bounded Boolean logics, Essential structure of proofs as a measure of complexity, New Curry-Howard terms for full linear logic, The explosion calculus, Completeness and cut-elimination for first-order ideal paraconsistent four-valued logic, Gentzen reduction revisited, Canonical signed calculi with multi-ary quantifiers, Encoding transition systems in sequent calculus, Reduction rules for intuitionistic \(\lambda\rho\)-calculus, Bilateralism does not provide a proof theoretic treatment of classical logic (for technical reasons), Reflecting rules: a note on generalizing the deduction theorem, Herbrand's fundamental theorem in the eyes of Jean van Heijenoort, Self-adjunctions and matrices., \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps, A minimal classical sequent calculus free of structural rules, A typed calculus based on a fragment of linear logic, A focused approach to combining logics, Categorical De Morgan laws, Grammar induction by unification of type-logical lexicons, Bounded memory Dolev-Yao adversaries in collaborative systems, A binary modal logic for the intersection types of lambda-calculus., Balzano's theory of ground and consequence, Nonmonotonic reasoning, preferential models and cumulative logics, A note on Gentzen's ordinal assignment, The consistency of arithmetic, Duality and the completeness of the modal \(\mu\)-calculus, Hilbert's epsilon as an operator of indefinite committed choice, Gödel's natural deduction, Logical foundations for programming semantics, A logic for category theory, Existential instantiation and normalization in sequent natural deduction, Theo: An interactive proof development system, General-elimination stability, Yet another bijection between sequent calculus and natural deduction, A symbolic model for timed concurrent constraint programming, Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus, A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, External and internal syntax of the \(\lambda \)-calculus, Resolution is cut-free, The multiple facets of the canonical direct unit implicational basis, Graded consequence revisited, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Semantic bootstrapping of type-logical grammar, Modal logics for communicating systems, An experimental logic based on the fundamental deduction principle, Quantifier-complete categories, On reduction rules, meaning-as-use, and proof-theoretic semantics, Phase transitions for Gödel incompleteness, Generating plans in linear logic. I: Actions as proofs, Generating plans in linear logic. II: A geometry of conjunctive actions, Truth-value semantics and functional extensions for classical logic of partial terms based on equality, Relevant analytic tableaux, The structure of multiplicatives, Coherence in Cartesian closed categories and the generality of proofs, Structured calculational proof, Harmonious logic: Craig's interpolation theorem and its descendants, The calculus of natural calculation, Permutability of proofs in intuitionistic sequent calculi, Intuitionism: an inspiration?, On the logic of unification, Logical structures and genus of proofs, Dual systems of tableaux and sequents for PLTL, Focusing and polarization in linear, intuitionistic, and classical logics, What is a (non-constructive) non-monotone logical system?, Correspondences between classical, intuitionistic and uniform provability, Proof finding algorithms for implicational logics, Falsification-aware semantics and sequent calculi for classical logic, Embedding friendly first-order paradefinite and connexive logics, Relative efficiency of propositional proof systems: Resolution vs. cut-free LK, An extended paradefinite logic combining conflation, paraconsistent negation, classical negation, and classical implication: how to construct Nice Gentzen-type sequent calculi, Maximum segments as natural deduction images of some cuts, Paraconsistent logics and translations, A proof description language and its reduction system, The complexity of the disjunction and existential properties in intuitionistic logic, ``Gaisi Takeuti's finitist standpoint and its mathematical embodiment, On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions, A proof-theoretic characterization of observational equivalence, On sequence-conclusion natural deduction systems, The structure of free closed categories, Simple consequence relations, Combining type disciplines, On the logical strength of the better quasi order with three elements, The elimination of maximum cuts in linear logic and BCK logic, Falsification-aware calculi and semantics for normal modal logics including S4 and S5, Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic, Supposition: A Problem for Bilateralism, On concurrent behaviors and focusing in linear logic, Formal metatheory of the lambda calculus using Stoughton's substitution, Dialogues and Proofs; Yankov’s Contribution to Proof Theory, Cut elimination for the unified logic, A NOTE ON FRAGMENTS OF UNIFORM REFLECTION IN SECOND ORDER ARITHMETIC, Applications of type theory, Gödel on deduction, Well-Ordering Principles in Proof Theory and Reverse Mathematics, Gentzen's consistency proof without heightlines, Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics, Antirealism, Meaning and Truth-Conditional Semantics, Game Semantics and the Manifestation Thesis, SEMANTIC POLLUTION AND SYNTACTIC PURITY, Uniform proofs as a foundation for logic programming, A deep inference system for the modal logic S5, A resource aware semantics for a focused intuitionistic calculus, A unified procedure for provability and counter-model generation in minimal implicational logic, Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology, On subexponentials, focusing and modalities in concurrent systems, Size-based termination of higher-order rewriting, AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ, Interpolation in extensions of first-order logic, ABSTRACT FORMS OF QUANTIFICATION IN THE QUANTIFIED ARGUMENT CALCULUS, RIGOUR AND PROOF, SUBATOMIC INFERENCES: AN INFERENTIALIST SEMANTICS FOR ATOMICS, PREDICATES, AND NAMES, An ecumenical notion of entailment, Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic, The Alf proof editor and its proof engine, Lorenzen's Proof of Consistency for Elementary Number Theory, Semantical analysis of the logic of bunched implications, Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications, Natural well-orderings, Characterizations of ordinal analysis, Adding Negation to Lambda Mu, A Logical Approach to Experience-Based Reasoning, On structural contraction and why it fails, On Inversion Principles, Computation with classical sequents, Non-elementary speed-ups in proof length by different variants of classical analytic calculi, Stanisław Jaśkowski and Natural Deduction Systems, First-order automated reasoning with theories: when deduction modulo theory meets practice, Focusing in Linear Meta-logic, What’s so Special About the Gödel Sentence $$\mathcal {G}$$ ?, NOMINALISTIC ORDINALS, RECURSION ON HIGHER TYPES, AND FINITISM, A fresh view of linear logic as a logical framework, Which Quantifiers Are Logical? A Combined Semantical and Inferential Criterion, A coinductive approach to proof search through typed lambda-calculi, Focused proof-search in the logic of bunched implications, Complexity among the finitely generated subgroups of Thompson's group, First-Degree Entailment and Structural Reasoning, Modal and intuitionistic variants of extended Belnap-Dunn logic with classical negation, An Isbell duality theorem for type refinement systems, Proof Terms for Generalized Natural Deduction, Distribution in the Logic of Meaning Containment and in Quantum Mechanics, Cut as Consequence, Method of Analysis: A Paradigm of Mathematical Reasoning?, Deforestation, program transformation, and cut-elimination, Towards Hilbert's 24th Problem: Combinatorial Proof Invariants, Polycategories, WEAK DISHARMONY: SOME LESSONS FOR PROOF-THEORETIC SEMANTICS, Correct Answers for First Order Logic, Learnability of type-logical grammars, Remarks on the Scott-Lindenbaum theorem, Conservative translations, A variant of Thomason's first-order logic CF based on situations, An open formalism against incompleteness, Subtractive logic, Die another day, Unnamed Item, The control layer in open mechanized reasoning systems: Annotations and tactics, Partitions and normal trees, Milestones from the Pure Lisp Theorem Prover to ACL2, Burali-Forti as a purely logical paradox, Prolegomena to any theory of proof simplicity, From mathematical axioms to mathematical rules of proof: recent developments in proof analysis, Informal and absolute proofs: some remarks from a Gödelian perspective, Decoding Gentzen's Notation, Least and Greatest Fixed Points in Linear Logic, Shallow confluence of conditional term rewriting systems, PURE LOGIC OF ITERATED FULL GROUND, PRESERVATION OF STRUCTURAL PROPERTIES IN INTUITIONISTIC EXTENSIONS OF AN INFERENCE RELATION, Prawitz, Proofs, and Meaning, Many-Valued Logics and Translations, Automating Soundness Proofs, PROOF-THEORETIC ANALYSIS OF THE QUANTIFIED ARGUMENT CALCULUS, Meta-entanglement, Normality, non-contamination and logical depth in classical natural deduction, Some pitfalls of LK-to-LJ translations and how to avoid them, Unnamed Item, Herbrand Sequent Extraction, On the Structure of Natural Deduction Derivations for “Generally”, Gödel, Gentzen, Goodstein: the magic sound of a G-string, … and so on: Schütte on Naming Ordinals, Well-ordering Principles, ω-models and $$ \varPi_{1}^{1} $$-comprehension, From Schütte’s Formal Systems to Modern Automated Deduction, Sequent Calculi for ‘Generally’, A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs, Modular sequent calculi for classical modal logics, Elaborating intersection and union types
