This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
The Use of Higher Order Logic in Program Verification
August 1976 (vol. 25 no. 8)
pp. 844-851
ASCII Text
x 
 
G.W. Ernst, R.J. Hookway, "The Use of Higher Order Logic in Program Verification," IEEE Transactions on Computers, vol. 25, no. 8, pp. 844-851, August, 1976.
 
 
BibTex
x
 
@article{ 10.1109/TC.1976.1674703,
author = {G.W. Ernst and R.J. Hookway},
title = {The Use of Higher Order Logic in Program Verification},
journal ={IEEE Transactions on Computers},
volume = {25},
number = {8},
issn = {0018-9340},
year = {1976},
pages = {844-851},
doi = {http://doi.ieeecomputersociety.org/10.1109/TC.1976.1674703},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - The Use of Higher Order Logic in Program Verification
IS - 8
SN - 0018-9340
SP844
EP851
EPD - 844-851
A1 - G.W. Ernst,
A1 - R.J. Hookway,
PY - 1976
KW - Heuristic search
KW - higher order logic
KW - inductive assertions
KW - mechanical theorem proving
KW - program verification.
VL - 25
JA - IEEE Transactions on Computers
ER -
 
G.W. Ernst, Department of Computer Engineering, Case Western Reserve University
This paper focuses on the interface between program verification and mechanical theorem proving. It is often much easier to express what a program does in higher order logic than in first-order logic. However, in general, higher order theorem proving is difficult to mechanize. Hence we have isolated some special classes of higher order formulas and will show how they can be processed efficiently by a computer. Examples are given that illustrate how naturally these formulas arise in program verification.
Index Terms:
Heuristic search, higher order logic, inductive assertions, mechanical theorem proving, program verification.
Citation:
G.W. Ernst, R.J. Hookway, "The Use of Higher Order Logic in Program Verification," IEEE Transactions on Computers, vol. 25, no. 8, pp. 844-851, Aug. 1976, doi:10.1109/TC.1976.1674703
Usage of this product signifies your acceptance of the Terms of Use.