First-Order Programming Theoriessowa <firstname.lastname@example.org>
Date: Sun, 4 Jul 93 18:02:29 EDT
From: sowa <email@example.com>
To: firstname.lastname@example.org, interlingua@ISI.EDU
Subject: First-Order Programming Theories
Since KIF and CGs are adopting a basically first-order semantics,
the question has come up about how far that will carry us in the
various problems that have to be addressed, in particular the
representation of procedures.
I recently came across a book that addresses some of those issues:
_First-Order Programming Theories_ by T. Gergely & L. Ury,
Springer-Verlag, 1991. Price $42.75. ISBN 3-540-54277-9.
Following is a quote from the Preface:
Many different approaches with different mathematical frameworks
have been proposed as a basis for programming theory.... Most of
[them] are related to mathematical logic and they provide their own
logic. Those logics, however, are very eclectic since they use
special entities to reflect a special world of programs, and also,
they are usually incomparable with each other. This Babel's mess
irritated us and we decided to peel off the eclectic components
and try to answer all the questions by using classical first-order
logic.... This work reflects our journey from the eclectic programming
logics to the simple classical first-order logic, which furthermore
turned out to be more powerful than the non-classical ones.
The book contains 351+ix pages in 26 chapters divided in 5 major parts:
Many-sorted first-order logic and model theory
Part I Computability
Part II Extended Dynamic Logics
Part III Temporal Characterization of Programs
Part IV Programming Logic with Explicit Time
In Part IV, the authors develop their version of "time logic", which
is a many-sorted FOL with time as one of the sorts. They show that
time logic is more general than (i.e. a refinement of) the dynamic
logics and temporal logics that they discussed in Parts II and III.
They do that by embedding both dynamic logic and temporal logic in
The book is not easy reading. It is notationally rather dense and
rather sparse in concrete examples and applications. However, the time
logic that it develops could be mapped into KIF and/or conceptual graphs
in a very direct way. Therefore, it is worth considering as a way of
handling procedures and programs in KIF and CGs.