Proof strategies in linear logic

DOI10.1007/BF00885763zbMath0821.03004OpenAlexW71891286MaRDI QIDQ1340963

Tanel Tammet

Publication date: 21 December 1994

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

algorithmslinear logicautomated theorem provingresolution methoddecision methods for fragments of linear logicproof search methods

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

On proof normalization in linear logic, Completeness of a first-order temporal logic with time-gaps, On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic, Unnamed Item, From multiple sequent for additive linear logic to decision procedures for free lattices, A new deconstructive logic: linear logic, Strong normalization for all-style LKtq, A resolution theorem prover for intuitionistic logic, Representing scope in intuitionistic deductions, Connection-based proof construction in linear logic, Resource-distribution via Boolean constraints, 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, Resolution calculus for the first order linear logic

Uses Software

• Lolli

Cites Work

• Linear logic
• Decision problems for propositional linear logic
• Resolution calculus for the first order linear logic
• Logic programming in a fragment of intuitionistic linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item