An Introduction to the Concepts and Techniques of Automated Theorem-Proving
| dc.contributor.author | Macock, Deborah Y. | en |
| dc.contributor.department | Computer Science | en |
| dc.date.accessioned | 2013-06-19T14:36:23Z | en |
| dc.date.available | 2013-06-19T14:36:23Z | en |
| dc.date.issued | 1975 | en |
| dc.description.abstract | This 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.mimetype | application/pdf | en |
| dc.identifier | http://eprints.cs.vt.edu/archive/00000803/ | en |
| dc.identifier.sourceurl | http://eprints.cs.vt.edu/archive/00000803/01/CS75024-R.pdf | en |
| dc.identifier.trnumber | CS75024-R | en |
| dc.identifier.uri | http://hdl.handle.net/10919/20271 | en |
| dc.language.iso | en | en |
| dc.publisher | Department of Computer Science, Virginia Polytechnic Institute & State University | en |
| dc.relation.ispartof | Historical Collection(Till Dec 2001) | en |
| dc.rights | In Copyright | en |
| dc.rights.uri | http://rightsstatements.org/vocab/InC/1.0/ | en |
| dc.title | An Introduction to the Concepts and Techniques of Automated Theorem-Proving | en |
| dc.type | Technical report | en |
| dc.type.dcmitype | Text | en |
Files
Original bundle
1 - 1 of 1