The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - April (1976 vol.25)
pp: 317-322
G.W. Ernst , Department of Computing and Information Sciences, Case Western Reserve University
ABSTRACT
This paper describes a theorem prover, running on a PDP-10-Tenex system, that can prove some theorems whose statements involve a relatively large number of definitions. Such theorems require special methods because 1) their statements contain a large number of clauses and 2) their proofs are quite long although straightforward.
INDEX TERMS
Artificial intelligence, heuristic search, higher order logic, mechanical theorem proving, natural deduction systems.
CITATION
G.W. Ernst, "A Definition-Driven Theorem Prover", IEEE Transactions on Computers, vol.25, no. 4, pp. 317-322, April 1976, doi:10.1109/TC.1976.1674611
14 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool