Condensed detachment is complete for relevance logic: A computer-aided proof (Q1181717): Difference between revisions
From MaRDI portal
Changed an Item |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 00:36, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Condensed detachment is complete for relevance logic: A computer-aided proof |
scientific article |
Statements
Condensed detachment is complete for relevance logic: A computer-aided proof (English)
0 references
27 June 1992
0 references
The condensed detachment rule \(D\) is a combination of modus ponens with a minimal amount of substitution. Earlier \(D\) has been shown to be complete for intuitionistic and classical implicational logic but incomplete for \(BCK\) and \(BCI\) logic. We show that \(D\) is complete for the relevance logic. One of the main steps is the proof of the formula \(((a\to a)\to a)\to a\) found in interaction with our resolution theorem prover. Various strategies of generating consequences of the axioms and choosing best ones for the next iteration were tried until the proof was found.
0 references
condensed detachment rule
0 references
relevance logic
0 references