Algebra of proofs
algebraic modelcompletenesscut-eliminationfunctional description of quantifiersintuitionistic first-order logicLindenbaum-Tarski algebrasproof theory
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Categorical logic, topoi (03G30) Research exposition (monographs, survey articles) pertaining to category theory (18-02) Foundations, relations to logic and deductive systems (18A15) Topoi (18B25) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- A cut-free Gentzen-type system for the logic of the weak law of excluded middle
- The linear abstract machine
- Algebra of constructions. I. The word problem for partial algebras
- A note on sequent calculi intermediate between LJ and LK
- Kohaerenz in Kategorien mit Gruppenstruktur
- Quantifier-complete categories
- A cut-elimination proof in intuitionistic predicate logic
- A maximal monoidal closed category of distributive algebraic domains
- On the semantics of the universal quantifier
- Proof of a conjecture of S. Mac Lane
- On categorical equivalence of Gentzen-style derivations in IMLL
- Sequent calculus for classical logic probabilized
- Cut elimination in categories
- Coherence via focusing for symmetric skew monoidal categories
- Categorical interpretation of logical derivations and its applications in algebra
- Multiplicative linear logics and fibrations
- Real Algebraic Strategies for MetiTarski Proofs
- Proposition algebra
- Multiquantaloids
- Proof-theoretical coherence
- scientific article; zbMATH DE number 4168913 (Why is no real title available?)
- Lambek vs. Lambek: functorial vector space semantics and string diagrams for Lambek calculus
- Algebre categoriali ed equazioni flessibili (una generalizzazione dell’ algebra universale)
- Lambek's categorical proof theory and Läuchli's abstract realizability
- scientific article; zbMATH DE number 1231636 (Why is no real title available?)
- Proof Complexity Meets Algebra
- Identity of Proofs Based on Normalization and Generality
- scientific article; zbMATH DE number 937370 (Why is no real title available?)
- Proof of a S.Mac Lane conjecture (extended abstract)
- Monoidal logics: completeness and classical systems
- Reversible monadic computing
- A Categorical Aspect of the Analogy Between Quantifiers and Modalities
- Algebraic proofs over noncommutative formulas
- Automata and coalgebras in categories of species
- Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories
- Deductive systems and coherence for skew prounital closed categories
- Coherence in Cartesian closed categories and the generality of proofs
- Functors of Lindenbaum-Tarski, schematic interpretations, and adjoint cylinders between sentential logics
This page was built for publication: Algebra of proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q788719)
