AUTOMATED THEOREM PROVING
Some major contributions to ATP classified by
philosophy of design
Logic
Presburger prover
Davis 1954
Bet.h tableau prover
Gilmore 1959
G"nt.zen-Herbrand prover
Hao Wang 1959
D-P procedure
Davis, Putnam 1980
Matching
Prawitz 1960
Resolution
Robinson 1964
(ccmtmuecl nat page}
Human Simulation
Logic Theory Macblne,
Newell. Shaw,
Simon 1957
Geometry Theorem
Pro'rin1 Machine,
Gelernter &aL1959
Semi-Automated Math.
Guard. Bennett,
Eut.on 1963-1967
Previous Page Next Page