First Order Programming Logic.
Robert Cartwright, John L. McCarthy:
First Order Programming Logic.
POPL 1979: 68-80@inproceedings{DBLP:conf/popl/CartwrightM79,
author = {Robert Cartwright and
John L. McCarthy},
title = {First Order Programming Logic},
booktitle = {POPL},
year = {1979},
pages = {68-80},
ee = {db/conf/popl/CartwrightM79.html},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
BibTeX
Abstract
First Order Programming Logic is a simple, yet powerful formal system for reasoning about recursive programs.
In its simplest form, it has one major limitation: it cannot establish any property of the least fixed point of a recursive program which is false for some other fixed point.
To rectify this weakness, we present two intuitively distinct approaches to strengthening First Order Programming Logic and prove that either extension makes the logic relatively complete.
In the process, we prove that the two approaches are formally equivalent.
The relative completeness of the extended logic is significant because it suggests it can establish all "ordinary" properties (obviously we cannot escape the Godelian incompleteness inherent in any programming logic) of recursive programs including those which compute partial functions.
Copyright © 1979 by the ACM,
Inc., used by permission. Permission to make
digital or hard copies is granted provided that
copies are not made or distributed for profit or
direct commercial advantage, and that copies show
this notice on the first page or initial screen of
a display along with the full citation.
POPL Proceedings Compendium
CDROM Version: Load the CDROM "POPL, The First Ten Years" and ...
BibTeX
Printed Edition
Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, January 1979.
ACM 1979 BibTeX
Contents
BibTeX
Copyright © Sat May 16 23:34:35 2009
by Michael Ley (ley@uni-trier.de)
