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.
Weitere Kapitel dieses Buchs durch Wischen aufrufen
- Semantic Trees in Automatic Theorem-Proving
P. J. Hayes
- Springer Berlin Heidelberg