The Markgraf Karl Refutation Procedure

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

The Markgraf Karl Refutation Procedure

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

Download BibTeX Cite

Proceedings of the Seventh International Joint Conference on Artificial Intelligence. Theorem Proving. 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.

Karl-Hans Bläsius, Norbert Eisinger, Jörg H. Siekmann, Gert Smolka, Alexander Herold, and Christoph Walther. 1981. The Markgraf Karl Refutation Procedure. In Proceedings of the Seventh International Joint Conference on Artificial Intelligence, IJCAI-81. IJCAI, 511–517. https://ijcai.org/proceedings/1981/96

@inproceedings{ijcai1981p96,
  title     = {The Markgraf Karl Refutation Procedure},
  author    = {Bläsius, Karl-Hans and Eisinger, Norbert and Siekmann, Jörg H. and Smolka, Gert and Herold, Alexander and Walther, Christoph},
  booktitle = {Proceedings of the Seventh International Joint Conference on
               Artificial Intelligence, {IJCAI-81}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Roger C. Schank},
  pages     = {511--517},
  year      = {1981},
  month     = {8},
  note      = {Theorem Proving},
  url       = {https://ijcai.org/proceedings/1981/96},
}

TY  - CPAPER
TI  - The Markgraf Karl Refutation Procedure
AU  - Bläsius, Karl-Hans
AU  - Eisinger, Norbert
AU  - Siekmann, Jörg H.
AU  - Smolka, Gert
AU  - Herold, Alexander
AU  - Walther, Christoph
T2  - Proceedings of the Seventh International Joint Conference on Artificial Intelligence, IJCAI-81
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1981
SP  - 511
EP  - 517
UR  - https://ijcai.org/proceedings/1981/96
ER  -