Resolution calculus for the first order linear logic

DOI10.1007/BF01051768zbMath0793.03006OpenAlexW2094862107MaRDI QIDQ1314284

Grigori Mints

Publication date: 22 February 1994

Published in: Journal of Logic, Language and Information (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01051768

zbMATH Keywords

completenessGentzen-type systemfirst order fragment of linear logicresolution-type calculi

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

Proof strategies in linear logic ⋮ Unnamed Item ⋮ From multiple sequent for additive linear logic to decision procedures for free lattices ⋮ Connection methods in linear logic and proof nets construction ⋮ Efficient resource management for linear logic proof search ⋮ Proof-search in type-theoretic languages: An introduction

Uses Software

• Lolli

Cites Work

• Linear logic
• Logic programming in a fragment of intuitionistic linear logic
• Proof strategies in linear logic
• The inverse method for establishing deducibility for logical calculi
• Uniform proofs as a foundation for logic programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item