Connection-based proof construction in linear logic

DOI10.1007/3-540-63104-6_20zbMath1430.03040OpenAlexW2124044295MaRDI QIDQ5234702

Heiko Mantel, Christoph Kreitz, 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

sequent calculuslinear logicsequent rule

Mathematics Subject Classification ID

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

Related Items

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

Uses Software

• Lolli

Cites Work

• A deductive solution for plan generation
• Linear logic
• The structure of multiplicatives
• Logic programming in a fragment of intuitionistic linear logic
• Proof strategies in linear logic
• On proof normalization in linear logic
• A uniform procedure for converting matrix proofs into sequent-style systems
• On Matrices with Connections
• An Efficient Unification Algorithm
• Logic Programming with Focusing Proofs in Linear Logic
• ileanTAP: An intuitionistic theorem prover
• T-string unification: Unifying prefixes in non-classical proof methods
• Converting non-classical matrix proofs into sequent-style systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item