Non-commutative proof construction: a constraint-based approach

DOI10.1016/J.APAL.2006.01.002MaRDI QIDQ2503402zbMATH OpenOpenAlexFDO

Authors Jean-Marc Andreoli, Roberto Maieli, Paul Ruet

Publication date 14 September 2006

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2006.01.002

zbMATH Keywords

cyclic linear logiclogical sequent calculinoncommutative logicproof construction

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Connection-based proof construction in non-commutative logic
• scientific article; zbMATH DE number 1231698
• Focussing and proof construction
• Non-commutative logic. III: Focusing proofs.
• scientific article; zbMATH DE number 1405459

Cites work

• A new constructive logic: classic logic
• A proof procedure for the logic of hereditary Harrop formulas
• An Efficient Unification Algorithm
• Focussing and proof construction
• Forum: A multiple-conclusion specification logic
• scientific article; zbMATH DE number 2134914 (Why is no real title available?)
• scientific article; zbMATH DE number 6157240 (Why is no real title available?)
• Logic programming in a fragment of intuitionistic linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Non-commutative logic II: sequent calculus and phase semantics
• Non-commutative logic. I: The multiplicative fragment
• Non-commutative logic. III: Focusing proofs.
• Quantales and (noncommutative) linear logic
• The Mathematics of Sentence Structure
• Une théorie combinatoire des séries formelles
• Uniform proofs as a foundation for logic programming

Cited in

(6)

• Focussing and proof construction
• Connection-based proof construction in non-commutative logic
• scientific article; zbMATH DE number 6829288 (Why is no real title available?)
• scientific article; zbMATH DE number 786497 (Why is no real title available?)
• Cyclic extensions of order varieties
• Algebraic proofs over noncommutative formulas

Describes a project that uses

Uses Software

• Lolli

This page was built for publication: Non-commutative proof construction: a constraint-based approach

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2503402)