On structuring proof search for first order linear logic

MaRDI QIDQ3408152zbMATH OpenFDO

Authors Paola Bruscoli, Alessio Guglielmi

Publication date 24 February 2010

zbMATH Keywords

cut eliminationfirst-order linear logicForumproof search

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• On structuring proof search for first order linear logic
• scientific article; zbMATH DE number 1499088
• Logic Programming with Focusing Proofs in Linear Logic
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• Focused proof search for linear logic in the calculus of structures

Cited in

(9)

• The number of proof lines and the size of proofs in first order logic
• Linear strategy for Boolean ring based theorem proving
• Formalization of linear space theory in the higher-order logic proving system
• On structuring proof search for first order linear logic
• scientific article; zbMATH DE number 1696770 (Why is no real title available?)
• Focused proof search for linear logic in the calculus of structures
• A first order system with finite choice of premises
• First-order Answer Set Programming as Constructive Proof Search
• scientific article; zbMATH DE number 1405458 (Why is no real title available?)

This page was built for publication: On structuring proof search for first order linear logic

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