Skip to main content

1983 | OriginalPaper | Buchkapitel

Semantic Trees in Automatic Theorem-Proving

verfasst von : R. Kowalski, P. J. Hayes

Erschienen in: Automation of Reasoning

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

We investigate in this paper the application of a modified version of semantic trees (Robinson 1968) to the problem of finding efficient rules of proof for mechanical theorem-proving. It is not our purpose to develop the general theory of these trees. We concentrate instead on those cases of semantic tree construction where we have found improvements of existing proof strategies. The paper is virtually self-contained and to the extent that it is not, Robinson’s review paper (1967) contains a clear exposition of the necessary preliminaries.

Metadaten
Titel
Semantic Trees in Automatic Theorem-Proving
verfasst von
R. Kowalski
P. J. Hayes
Copyright-Jahr
1983
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-642-81955-1_13

Neuer Inhalt