Switch to: References

Citations of:

Algebra of proofs

New York: sole distributors for the U.S.A. and Canada, Elsevier North-Holland (1978)

Add citations

You must login to add citations.
  1. Lambek vs. Lambek: Functorial vector space semantics and string diagrams for Lambek calculus.Bob Coecke, Edward Grefenstette & Mehrnoosh Sadrzadeh - 2013 - Annals of Pure and Applied Logic 164 (11):1079-1100.
    The Distributional Compositional Categorical model is a mathematical framework that provides compositional semantics for meanings of natural language sentences. It consists of a computational procedure for constructing meanings of sentences, given their grammatical structure in terms of compositional type-logic, and given the empirically derived meanings of their words. For the particular case that the meaning of words is modelled within a distributional vector space model, its experimental predictions, derived from real large scale data, have outperformed other empirically validated methods that (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • Sequent calculus for classical logic probabilized.Marija Boričić - 2019 - Archive for Mathematical Logic 58 (1-2):119-136.
    Gentzen’s approach to deductive systems, and Carnap’s and Popper’s treatment of probability in logic were two fruitful ideas that appeared in logic of the mid-twentieth century. By combining these two concepts, the notion of sentence probability, and the deduction relation formalized in the sequent calculus, we introduce the notion of ’probabilized sequent’ \ with the intended meaning that “the probability of truthfulness of \ belongs to the interval [a, b]”. This method makes it possible to define a system of derivations (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • A cut-free gentzen-type system for the logic of the weak law of excluded middle.Branislav R. Boričić - 1986 - Studia Logica 45 (1):39-53.
    The logic of the weak law of excluded middleKC p is obtained by adding the formula A A as an axiom scheme to Heyting's intuitionistic logicH p . A cut-free sequent calculus for this logic is given. As the consequences of the cut-elimination theorem, we get the decidability of the propositional part of this calculus, its separability, equality of the negationless fragments ofKC p andH p , interpolation theorems and so on. From the proof-theoretical point of view, the formulation presented (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • Cut Elimination in Categories.Kosta Došen - 1999 - Dordrecht, Netherland: Springer.
    Proof theory and category theory were first drawn together by Lambek some 30 years ago but, until now, the most fundamental notions of category theory have not been explained systematically in terms of proof theory. Here it is shown that these notions, in particular the notion of adjunction, can be formulated in such as way as to be characterised by composition elimination. Among the benefits of these composition-free formulations are syntactical and simple model-theoretical, geometrical decision procedures for the commuting of (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • Variable truth.M. E. Szabo - 1984 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 30 (26‐29):401-414.
    Direct download  
     
    Export citation  
     
    Bookmark  
  • The continuous realizability of entailment.M. E. Szabo - 1983 - Mathematical Logic Quarterly 29 (4):219-233.
  • Hyperdoctrines, Natural Deduction and the Beck Condition.Robert A. G. Seely - 1983 - Mathematical Logic Quarterly 29 (10):505-542.
  • Monoidal logics: completeness and classical systems.Clayton Peterson - 2019 - Journal of Applied Non-Classical Logics 29 (2):121-151.
    ABSTRACTMonoidal logics were introduced as a foundational framework to analyze the proof theory of logical systems. Inspired by Lambek's seminal work in categorical logic, the objective is to defin...
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  • An interpretation of classical proofs.Glen Helman - 1983 - Journal of Philosophical Logic 12 (1):39 - 71.
  • Modal translations in substructural logics.Kosta Došen - 1992 - Journal of Philosophical Logic 21 (3):283 - 336.
    Substructural logics are logics obtained from a sequent formulation of intuitionistic or classical logic by rejecting some structural rules. The substructural logics considered here are linear logic, relevant logic and BCK logic. It is proved that first-order variants of these logics with an intuitionistic negation can be embedded by modal translations into S4-type extensions of these logics with a classical, involutive, negation. Related embeddings via translations like the double-negation translation are also considered. Embeddings into analogues of S4 are obtained with (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  • Bicartesian coherence.Kosta Došen & Zoran Petrić - 2002 - Studia Logica 71 (3):331 - 353.
    Coherence is demonstrated for categories with binary products and sums, but without the terminal and the initial object, and without distribution. This coherence amounts to the existence of a faithful functor from a free category with binary products and sums to the category of relations on finite ordinals. This result is obtained with the help of proof-theoretic normalizing techniques. When the terminal object is present, coherence may still be proved if of binary sums we keep just their bifunctorial properties. It (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  • The Development of Categorical Logic.John L. Bell - unknown
    5.5. Every topos is linguistic: the equivalence theorem.
     
    Export citation  
     
    Bookmark   7 citations