Solving a Problem in Relevance Logic with an Automated Theorem Prover
A new challenging problem for automated theorem provers (ATP) is presented. It is from the field of relevance logic and is known as “converse of contraction”. We firstly give some background informatlon about relevance logic and the problem itself and then discuss a proof for the theorem which has been found by the Markgraf Karl Refutation Procedure (MKRP), a resolution based theorem prover, under development at the Universities of Karlsruhe and Kaiserslautern.
For solving this problem we implemented a new method to control the application of “generator clauses” like Exy ⇒ Ef(x)f(y). An uncontrolled application of such clauses produces arbitrarily deeply nested and often useless terms f (f (f (f ... which in general cannot be avoided with a global term depth limit because deeply nested terms of more heterogenous structure may occur in the proof.
KeywordsRelevance Logic Automate Theorem Prover Unit Clause Generator Clause Connection Graph
Unable to display preview. Download preview PDF.
- [AB 75]A.R. Anderson, N.D. Belnap Entailment: The Logic of Relevance and Necessity Vol. 1, Princeton University Press, 1975Google Scholar
- [AO 83]G. Antoniou, H.J. Ohlbach Terminator Proc. of Eights IJCAI, Karlsruhe 1983Google Scholar
- [E 81]N. Eisinger Subsumption and Connection Graphs Proc. of GWAI-81, Bad Honnef 1981Google Scholar
- [HR 78]
- [KMR83]Karl Mark G. Raph The Markgraf. Karl Refutatlon Procedure: Spring 1983 University of Karlsruhe, Interner BerlchtGoogle Scholar
- [KO 75]
- [MW 76]G.A. Wilson, J. Minker Resolution Refinement and Search Strategies: A Comparative Study. Trans. on Comp., vol. C-25, no.8, 1976Google Scholar
- [OW 83]R. Overbeck, L. Wos Private Communication (IJCAI 83)Google Scholar
- [wA 81]C. Walther Elimination of Redundant Links in Extended Connection Graphs. University of Karlsruhe, Interner Bericht 10/81Google Scholar
- [RM 72]R. Routley, R. Meyer The Semantics of Entailment in Truth, Syntax and Modality. Leblanc (ed) North-Holland 1972Google Scholar