---
title: "The Markgraf Karl Refutation Procedure"
authors:
  - "Karl-Hans Bläsius"
  - "Norbert Eisinger"
  - "Jörg H. Siekmann"
  - "Gert Smolka"
  - "Alexander Herold"
  - "Christoph Walther"
doi: ""
url: "https://ijcai.org/proceedings/1981/96"
pdf: "https://ijcai.org/proceedings/1981/0096.pdf"
venue: "Proceedings of the Seventh International Joint Conference on Artificial Intelligence"
year: 1981
pages: "511-517"
track: "Theorem Proving"
keywords:
---

# The Markgraf Karl Refutation Procedure

Karl-Hans Bläsius, Norbert Eisinger, Jörg H. Siekmann, Gert Smolka, Alexander Herold, Christoph Walther

*Proceedings of the Seventh International Joint Conference on Artificial Intelligence*, pages 511-517.

## Abstract

The cuPrent st a te of a TheoPem Proving Sy s te m (The MaPkgmf KaPt Refutation FPocedure) at the Unive Psity of KaPtsPUh e is pPesented. The goat of this pPojec t c an be swrurrJ.rized by the fotl-owing thPee cl- aims: i t is possibLe to progpam a theoPem proveP ( TPJ and augment it by appPopPiate heuristics and do main-specific knowLedge such that (iJ it witt displ-ay an 'active' and directed behavi o UP in its striving foP a pPoof, PatheP than th e 'passive' combinatorial- seaPChthPough ve ry t a Pg e seaPch spaces, which was the chaPa ct e risti c behaviouP of the TPs of the past. Consequentl-y (ii) it witt not genePate a seaPCh space of many thousands of iPPetevant cl-auses, but witt find a proof with comparativel-y few Pedundant dePivat io n steps. (iii) Such a TP witt establ-ish an unprecedented l-eap in pePformance oveP previous TPs e;rppessed in terms of the difficuLty of the theoPems it can prove. The resuLts obtained thus far coPPOboPate the first two cl aims.