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
• Foundations of proof search strategies design in linear logic
• 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
• Proof-search in implicative linear logic as a matching problem
• 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
• Resource management in linear logic proof search revisited

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)