Condensed detachment is complete for relevance logic: A computer-aided proof
From MaRDI portal
Publication:1181717
DOI10.1007/BF01880330zbMath0751.03011OpenAlexW2053760476MaRDI QIDQ1181717
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
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
This page was built for publication: Condensed detachment is complete for relevance logic: A computer-aided proof