Proof finding algorithms for implicational logics
type: Item
instance of: scholarly article
title: Proof finding algorithms for implicational logics
zbMATH Open document ID: 0972.03022
DOI: 10.1016/S0304-3975(99)00174-7
published in: Theoretical Computer Science
publication date: 2000-08-23T00:00:00Z
review text: Logics considered here include implicational fragments of intuitionistic propositional logic, relevance logics \(R_{\rightarrow}\), \(T_{\rightarrow}\) and \(T_{\rightarrow}-W\), multiplicative linear logic and affine logic. For each of them a restriction on \(\lambda\)-terms providing an equivalent natural deduction formulation is stated, then a corresponding proof search algorithm is described.
Mathematics Subject Classification ID: 03B47
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 1495205
zbMATH Keywords: implicative logics
zbMATH Keywords: decision procedures
zbMATH Keywords: implicational fragments
zbMATH Keywords: intuitionistic propositional logic
zbMATH Keywords: relevance logics
zbMATH Keywords: multiplicative linear logic
zbMATH Keywords: affine logic
zbMATH Keywords: restriction on \(\lambda\)-terms
zbMATH Keywords: natural deduction
zbMATH Keywords: proof search algorithm
author: Martin W. Bunder
reviewed by: G. E. Mints
MaRDI profile type: Publication
cites work: Q4085699
cites work: Lambda terms definable as combinators
cites work: Q5610986
cites work: BCK and BCI logics, condensed detachment and the 2-property
cites work: Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt
cites work: Intuitionistic propositional logic is polynomial-space complete
Recommended article: Proof-finding algorithms for classical and subclassical propositional logics
Recommended article: An algorithm for the class of pure implicational formulas
Recommended article: Q2767024
Recommended article: Q3476786
Recommended article: Q4829322
Recommended article: A proof-search procedure for intuitionistic propositional logic
Recommended article: Algorithmic proof methods and cut elimination for implicational logics. I: Modal implication
Recommended article: Proof complexity of intuitionistic implicational formulas
Recommended article: Proof-search in intuitionistic logic based on constraint satisfaction
Recommended article: Q4934557
description: scientific article; zbMATH DE number 1495205