Condensed detachment is complete for relevance logic: A computer-aided proof

DOI10.1007/BF01880330zbMath0751.03011OpenAlexW2053760476MaRDI QIDQ1181717

Tanel Tammet, Grigori Mints

Publication date: 27 June 1992

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

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

zbMATH Keywords

relevance logiccondensed detachment rule

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Related Items

A finitely axiomatized formalization of predicate calculus with equality, Using resolution for deciding solvable classes and building finite models, Principal type-schemes of BCI-lambda-terms, The converse principal type-scheme theorem in lambda calculus, Principal types of BCK-lambda-terms, Double-negation elimination in some propositional logics

Cites Work

• Unnamed Item
• Maslov's inverse method and decidable classes
• Combinatory logic. With two sections by William Craig.
• The semantics and proof theory of linear logic
• Completeness of the normal typed fragment of the \(\lambda\)-system \(U\)
• Principal type-schemes and condensed detachment
• A Machine-Oriented Logic Based on the Resolution Principle
• The Principal Type-Scheme of an Object in Combinatory Logic
• Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt