This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
August 1976 (vol. 25 no. 8)
pp. 769-772
L.J. Henschen, Department of Computer Sciences, North-western University
Automated theorem proving involves the programming of computers to perform logical (mathematical) deduction. This should not be confused with numerical calculation, in which operations that need to be performed can be exactly specified ahead of time as, for example, in Gaussian elimination. Rather, theorem provers search for proofs of statements given axioms describing the basic assumptions such as would occur in a modern algebra text on group theory. There are many theorem-proving programs that are based on ad hoc data representations and manipulations;many such techniques are derived by the programmer analyzing how he himself proves theorems. However, the most widely studied and best understood general method is based on the resolution principle for first-order logic of Robinson [9]. Indeed, all the papers in this issue have resolution as a starting point.
Citation:
L.J. Henschen, "Introduction Tutorial on Resolution," IEEE Transactions on Computers, vol. 25, no. 8, pp. 769-772, Aug. 1976, doi:10.1109/TC.1976.1674695
Usage of this product signifies your acceptance of the Terms of Use.