Title :
A Definition-Driven Theorem Prover
Author :
Ernst, George W.
Author_Institution :
Department of Computing and Information Sciences, Case Western Reserve University
fDate :
4/1/1976 12:00:00 AM
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.
Keywords :
Artificial intelligence, heuristic search, higher order logic, mechanical theorem proving, natural deduction systems.; Filters; Helium; Logic; Man machine systems; Military computing; Artificial intelligence, heuristic search, higher order logic, mechanical theorem proving, natural deduction systems.;
Journal_Title :
Computers, IEEE Transactions on
DOI :
10.1109/TC.1976.1674611
