Condensed detachment is complete for relevance logic: A computer-aided proof. (English) Zbl 0751.03011
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.
Reviewer: G.Mints (Stanford)
MSC:
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
| 03B35 | Mechanization of proofs and logical operations |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03-04 | Software, source code, etc. for problems pertaining to mathematical logic and foundations |
References:
| [1] | Avron A., ’The semantics and proof-theory of linear logic’,Theoretical Computer Science 57, 161–189 (1988). · Zbl 0652.03018 · doi:10.1016/0304-3975(88)90037-0 |
| [2] | Anderson, A. R. and Belnap, N. D.,Entailment, Vol. I, Princeton University Press (1975). |
| [3] | Church, A., ’The weak theory of implication’, inKontrolliertes Denken, Untersuchungen zum Logikkalkül und zur Logik der Einzelwissenschaften (Festgabe zum 60. Geburtstag von Prof. W. Britzelmayr), A. Menne, A. Wilhelmy, and H. Angstl (eds.), München Kommissionverlag Karl Aber, pp. 22–37 (1951). |
| [4] | Curry, H. B. and Feys, R.,Combinatorial Logic, Vol. I, North-Holland (1958). · Zbl 0081.24104 |
| [5] | Girard, J.-Y., ’Linear logic’,Theoretical Computer Science,N1, (1987). |
| [6] | Helman, G. H., ’Restricted lambda abstraction and the interpretation of some non-classical logics’, Ph.D. Dissertation, University of Pittsburgh (1977), University Microfilms, Ann Arbor, iv + 217 pp. · Zbl 0355.02017 |
| [7] | Hindley J. R., ’The principal type-scheme of an object in combinatory logic’,Trans. Amer. Math. Soc. 146, 29–60 (1969). · Zbl 0196.01501 |
| [8] | Hindley, J. R. and Meredith, D., ’Principal type-schemes and condensed detachment’. Preprint, October (1987). · Zbl 0708.03007 |
| [9] | Jaśkowski S., Über Tautologien in welchen keine Variable mehr als zweimal vorkommt’,Zeitschrift für Math. Logik und Grundlagen der Math 9, 219–228 (1963). · Zbl 0115.00501 · doi:10.1002/malq.19630091206 |
| [10] | Martins, J. P. and Shapiro, S. C., ’A model for belief revision’,Non-Monotonic Reasoning Workshop pp. 241–294 (1984). |
| [11] | Moh Shaw-Kwei, ’The deduction theory and two new logical systems’,Methodos 2, 56–75 (1950). |
| [12] | Robinson J. A., ’A machine-oriented logic based on the resolution principle’,J. Ass. Computing Machinery 12, 23–4 (1965). · Zbl 0139.12303 |
| [13] | Tammet, T., ’The resolution program, able to decide some sovable classes’.COLOG-88: International Conference on Computer Logic. Proceedings. LNCS, v. 417, Springer-Verlag, pp. 300–312 (1990). · Zbl 0727.03009 |
| [14] | Wos, L., Overbeek, R., Lusk, E., and Boyle, J.,Automated Reasoning, Prentice-Hall (1984). |
| [15] | Zamov N. K., ’Maslov’s inverse method and decidable classes’,Annals of Pure and Applied Logic 42, 165–194 (1989). · Zbl 0692.03009 · doi:10.1016/0168-0072(89)90053-5 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
