The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.08 - August (1976 vol.25)
pp: 769-772
L.J. Henschen , Department of Computer Sciences, North-western University
ABSTRACT
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.
INDEX TERMS
null
CITATION
L.J. Henschen, "Introduction Tutorial on Resolution", IEEE Transactions on Computers, vol.25, no. 8, pp. 769-772, August 1976, doi:10.1109/TC.1976.1674695
15 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool