Name
Abstract | ||
|---|---|---|
The condensed detachment ruleD is a combination of modus ponens with a minimal amount of substitution. EarlierD has been shown to be complete for intuitionistic and classical implicational logic but incomplete forBCK andBCI logic. We show thatD is complete for the relevance logic. One of the main steps is the proof of the formula ((a ?a) ?a) ?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. |
Year | DOI | Venue |
|---|---|---|
1991 | 10.1007/BF01880330 | J. Autom. Reasoning |
Keywords | Field | DocType |
Automated theorem proving,relevance logic,condensed detachment | Discrete mathematics,Deduction theorem,Modus ponens,Axiom,Computer-aided,Automated theorem proving,Algorithm,Relevance logic,Condensed detachment,Mathematics,Direct proof | Journal |
Volume | Issue | ISSN |
7 | 4 | 1573-0670 |
Citations | PageRank | References |
4 | 0.70 | 7 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Grigori Mints | 1 | 235 | 72.76 |
| Tanel Tammet | 2 | 199 | 91.61 |