Connection-based proof construction in linear logic

DOI10.1007/3-540-63104-6_20MaRDI QIDQ5234702zbMATH OpenOpenAlexFDO

Authors Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt

Publication date 1 October 2019

Published in Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-63104-6_20

zbMATH Keywords

linear logicsequent calculussequent rule

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• scientific article; zbMATH DE number 1301753
• A matrix characterization for multiplicative exponential linear logic
• Connection methods in linear logic and proof nets construction
• scientific article; zbMATH DE number 1543301
• scientific article; zbMATH DE number 1324433

Cites work

• \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
• A deductive solution for plan generation
• A uniform procedure for converting matrix proofs into sequent-style systems
• An Efficient Unification Algorithm
• Converting non-classical matrix proofs into sequent-style systems
• scientific article; zbMATH DE number 18649 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 1324433 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• scientific article; zbMATH DE number 937366 (Why is no real title available?)
• scientific article; zbMATH DE number 3359806 (Why is no real title available?)
• Linear logic
• Logic programming in a fragment of intuitionistic linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• On Matrices with Connections
• On proof normalization in linear logic
• Proof strategies in linear logic
• T-string unification: unifying prefixes in non-classical proof methods
• The structure of multiplicatives

Cited in

(11)

• Connection methods in linear logic and proof nets construction
• Proof-search in type-theoretic languages: An introduction
• A uniform procedure for converting matrix proofs into sequent-style systems
• A matrix characterization for multiplicative exponential linear logic
• Proof reconstruction in classical and nonclassical logics (Diss., TU Darmstadt, 1999)
• scientific article; zbMATH DE number 1696770 (Why is no real title available?)
• scientific article; zbMATH DE number 1301753 (Why is no real title available?)
• scientific article; zbMATH DE number 1341478 (Why is no real title available?)
• scientific article; zbMATH DE number 1543301 (Why is no real title available?)
• Construction of retractile proof structures
• Connection calculus theorem proving with multiple built-in theories

Describes a project that uses

Uses Software

• Lolli

This page was built for publication: Connection-based proof construction in linear logic

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