Solving a Problem in Relevance Logic with an Automated Theorem Prover

  • Hans-Jürgen Ohlbach
  • Graham Wrightson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


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.


Relevance Logic Automate Theorem Prover Unit Clause Generator Clause Connection Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AB 75]
    A.R. Anderson, N.D. Belnap Entailment: The Logic of Relevance and Necessity Vol. 1, Princeton University Press, 1975Google Scholar
  2. [AO 83]
    G. Antoniou, H.J. Ohlbach Terminator Proc. of Eights IJCAI, Karlsruhe 1983Google Scholar
  3. [E 81]
    N. Eisinger Subsumption and Connection Graphs Proc. of GWAI-81, Bad Honnef 1981Google Scholar
  4. [HR 78]
    M.C. Harrison, N. Rubin Another Generalization of Resolution JACM 25:3 341–351 1978MathSciNetCrossRefzbMATHGoogle Scholar
  5. [KMR83]
    Karl Mark G. Raph The Markgraf. Karl Refutatlon Procedure: Spring 1983 University of Karlsruhe, Interner BerlchtGoogle Scholar
  6. [KO 75]
    R. Kowalski A Proof Procedure Using Connection Graphs JACM 22:4 1975MathSciNetCrossRefzbMATHGoogle Scholar
  7. [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
  8. [OW 83]
    R. Overbeck, L. Wos Private Communication (IJCAI 83)Google Scholar
  9. [wA 81]
    C. Walther Elimination of Redundant Links in Extended Connection Graphs. University of Karlsruhe, Interner Bericht 10/81Google Scholar
  10. [RM 72]
    R. Routley, R. Meyer The Semantics of Entailment in Truth, Syntax and Modality. Leblanc (ed) North-Holland 1972Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Hans-Jürgen Ohlbach
    • 1
  • Graham Wrightson
    • 2
  1. 1.Institut für Informatik IUniversity of KaiserslauternKaiserslautern
  2. 2.Dep. of Computer ScienceVictoria UniversityWellingtonNew Zealand

Personalised recommendations