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