Resolution calculus for the first order linear logic
type: Item
instance of: scholarly article
title: Resolution calculus for the first order linear logic
zbMATH Open document ID: 0793.03006
DOI: 10.1007/BF01051768
published in: Journal of Logic, Language and Information
publication date: 1994-02-22T00:00:00Z
review text: This paper presents a formulation and completeness proof of the resolution-type calculi for the first order fragment of Girard's linear logic by a general method which provides the general scheme of transforming a cut-free Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. Ideas of the author and Zamov are used to avoid Skolemization. Completeness of strategies is first established for the Gentzen-type system, and then transferred to resolution. The propositional resolution sustem was implemented by \textit{T. Tammet} [``Proof search strategies for linear logic'', J. Autom. Reasoning (to appear)]. This computer program was successful due to several additional strategies derived from the connection with Gentzen-type systems.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B20
zbMATH DE Number: 501106
zbMATH Keywords: first order fragment of linear logic
zbMATH Keywords: completeness
zbMATH Keywords: resolution-type calculi
zbMATH Keywords: Gentzen-type system
author: G. E. Mints
reviewed by: G. E. Mints
describes a project that uses: Lolli
MaRDI profile type: Publication
cites work: Linear logic
cites work: Logic programming in a fragment of intuitionistic linear logic
cites work: The inverse method for establishing deducibility for logical calculi
cites work: Q5639373
cites work: Uniform proofs as a foundation for logic programming
cites work: Q3768867
cites work: Q3972527
cites work: Q4281258
cites work: Proof strategies in linear logic
cites work: Q3777987
full work available at URL: https://doi.org/10.1007/bf01051768
OpenAlex ID: W2094862107
description: scientific article; zbMATH DE number 501106