Proceedings Article, Paper @InProceedings Beitrag in Tagungsband, Workshop

 Show entries of: this year (2019) | last year (2018) | two years ago (2017) | Notes URL
 Action: login to update Options: Library locked Goto entry point

 Author, Editor
 Author(s): Ohlbach, Hans Jürgen Siekmann, Jörg H. dblp dblp
 Editor(s): Lassez, J. L. Plotkin, Gordon dblp dblp
 BibTeX cite key*: OhlbachSiekmann91a

 Title, Booktitle
 Title*: The Markgraf Karl Refutation Procedure Booktitle*: Computational Logic, Essays in Honor of Alan Robinson

 Event, URLs
 URL of the conference: URL for downloading the paper: Event Address*: ? Language: English Event Date* (no longer used): ? Organization: Event Start Date: 16 September 2019 Event End Date: 16 September 2019

 Publisher
 Name*: MIT Press URL: Address*: Cambridge, USA Type:

 Vol, No, Year, pp.
 Series:
 Volume: Number: Month: Pages: 41-112 Year*: 1991 VG Wort Pages: ISBN/ISSN: Sequence Number: DOI:

 (LaTeX) Abstract: The goal of the {\em MKRP project} is the development of a theorem prover which can be used as an inference engine in various applications, in particular it should be capable of proving significant mathematical theorems. Our first implementation, the {\em Markgraf Karl Refutation Procedure (MKRP)} realizes some of the ideas we have developed to this end. It is a general purpose resolution based deduction system that exploits the representation of formulae as a graph (clause graph). The main features are its well tailored selection components, heuristics and control mechanisms for guiding the search for a proof. mechanisms for guiding the search for a proof. This paper gives an overview of the system. It summarizes and evaluates our experience with the system in particular, and the logics we use as well as the clause graph approach: as 1990 marks the fifteenth birthday of the system, the time may have come to ask: Was it worth the effort?'' Download Access Level:

 Correlation
 MPG Unit: Max-Planck-Institut für Informatik MPG Subunit: Programming Logics Group Audience: experts only Appearance:

BibTeX Entry:

@INPROCEEDINGS{OhlbachSiekmann91a,
AUTHOR = {Ohlbach, Hans J{\"u}rgen and Siekmann, J{\"o}rg H.},
EDITOR = {Lassez, J. L. and Plotkin, Gordon},
TITLE = {The {Markgraf Karl} Refutation Procedure},
BOOKTITLE = {Computational Logic, Essays in Honor of Alan Robinson},
PUBLISHER = {MIT Press},
YEAR = {1991},
PAGES = {41--112},
}