Abstract
This report presents a quick overview of the Markgraf Karl Refutation Procedure, an automated theorem prover (TP) currently under development at the University of Karlsruhe, and then concentrates in detail on those parts of the system, which presently determine the choice of the deduction steps to be performed by the system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
J. Siekmann, G. Smolka: Selection Heuristics, Deletion Strategies and N-Level Terminator Configurations for the Connection Graph Proof Procedure. Universität Karlsruhe, Research Report, 1981.
N. Eisinger: Subsumption and Connection Graphs. Universität Karlsruhe, Research Report, 1981.
N. Eisinger, J. Siekmann, G. Smolka, E. Unvericht, C. Walther: The Markgraf Karl Refutation Procedure (FALL 1980). Universität Karlsruhe, Research Report, 1981.
N. Eisinger, P. Kursawe, J. Siekmann, G. Smolka, C. Walther: The Markgraf Karl Refutation Procedure: USER MANUAL. Universität Karlsruhe, Research Report, 1981.
C. Walther: Elimination of Redundant Links in Extended Connection Graphs. Universität Karlsruhe, Research Report, 1981.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1981 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Siekmann, J., Smolka, G. (1981). Selection Heuristics, Deletion Strategies and N-Level Terminator Configurations for the Connection Graph Proof Procedure. In: Siekmann, J.H. (eds) GWAI-81. Informatik-Fachberichte, vol 47. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-02328-0_18
Download citation
DOI: https://doi.org/10.1007/978-3-662-02328-0_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-10859-7
Online ISBN: 978-3-662-02328-0
eBook Packages: Springer Book Archive