Browsing by Author "Macock, Deborah Y."

Now showing 1 - 3 of 3
  • Thumbnail Image
    Automated Theorem-proving and Program Verification: An Annotated Bibliography
    Macock, Deborah Y. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1975)
    This bibliography contains a synopsis of each reference, taken from one of three sources: (1) the author's abstract; (2) the review of the reference in ACM Computing Reviews; (3) an abstract prepared locally. The third alternative was chosen only if the first two were unavailable. Each reference is identified by a number with prefix PV or A (program verification or automated theorem-proving) depending upon its contents, and the identification number is used for cross-referencing the entries. If a reference deals with both areas, it has two identification numbers. Also included is an author index, which is arranged alphabetically according to the first author's name if the source is co-authored. It is anticipated that this bibliography will be updated as research in the field progresses.
  • Thumbnail Image
    An Introduction to the Concepts and Techniques of Automated Theorem-Proving
    Macock, Deborah Y. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1975)
    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.
  • Thumbnail Image
    The Requirements for Effective Hardware Description Languages
    Lee, John A. N.; Macock, Deborah Y.; Marks, Peter; Wesselkamper, Thomas C. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1975)
    The design of hardware description languages (HDL's) is considered with respect to their structural and functional properties rather than their syntactic forms. The contents of an idealized HDL are contrasted with those of nine existing languages, chosen so as to typify a wide range of usage, numerous citations in the literature, and a diversity of source.