An Introduction to the Concepts and Techniques of Automated Theorem-Proving

Simple item page
dc.contributor.authorMacock, Deborah Y.en
dc.contributor.departmentComputer Scienceen
dc.date.accessioned2013-06-19T14:36:23Zen
dc.date.available2013-06-19T14:36:23Zen
dc.date.issued1975en
dc.description.abstractThis paper summarizes the theoretical foundations and basic methodology of automated theorem-proving. The material presented includes a review of the predicate calculus, the transformation of a first-order wff into clause normal form, J. A. Robinson's resolution principle, semantic resolution, significant resolution heuristics (search strategies), and paramodulation. The application of theorem-proving techniques to the problem of program correctness is also briefly discussed.en
dc.format.mimetypeapplication/pdfen
dc.identifierhttp://eprints.cs.vt.edu/archive/00000803/en
dc.identifier.sourceurlhttp://eprints.cs.vt.edu/archive/00000803/01/CS75024-R.pdfen
dc.identifier.trnumberCS75024-Ren
dc.identifier.urihttp://hdl.handle.net/10919/20271en
dc.language.isoenen
dc.publisherDepartment of Computer Science, Virginia Polytechnic Institute & State Universityen
dc.relation.ispartofHistorical Collection(Till Dec 2001)en
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.titleAn Introduction to the Concepts and Techniques of Automated Theorem-Provingen
dc.typeTechnical reporten
dc.type.dcmitypeTexten

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
CS75024-R.pdf
Size:
1.18 MB
Format:
Adobe Portable Document Format
Download

Collections

Computer Science Technical Reports