Condensed detachment is complete for relevance logic: A computer-aided proof
DOI10.1007/BF01880330zbMATH Open0751.03011OpenAlexW2053760476MaRDI QIDQ1181717FDOQ1181717
Authors: Tanel Tammet, G. E. 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
Recommendations
Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)
Cites Work
- The semantics and proof theory of linear logic
- Combinatory logic. With two sections by William Craig.
- A Machine-Oriented Logic Based on the Resolution Principle
- The Principal Type-Scheme of an Object in Combinatory Logic
- Maslov's inverse method and decidable classes
- Principal type-schemes and condensed detachment
- Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt
- Completeness of the normal typed fragment of the \(\lambda\)-system \(U\)
- Title not available (Why is that?)
Cited In (11)
- The converse principal type-scheme theorem in lambda calculus
- Principal types of BCK-lambda-terms
- Title not available (Why is that?)
- Note on D-completeness and prelinearity
- A simplified form of condensed detachment
- Principal type-schemes of BCI-lambda-terms
- Using resolution for deciding solvable classes and building finite models
- Condensed detachment as a rule of inference
- A finitely axiomatized formalization of predicate calculus with equality
- The two-property and condensed detachment
- Double-negation elimination in some propositional logics
This page was built for publication: Condensed detachment is complete for relevance logic: A computer-aided proof
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1181717)
