First-Order Programming Theories

sowa <sowa@turing.pacss.binghamton.edu>
Date: Sun, 4 Jul 93 18:02:29 EDT
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9307042202.AA04657@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU
Subject: First-Order Programming Theories
Cc: sowa@turing.pacss.binghamton.edu

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:

   Mathematical Background

     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
time logic.

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.

John Sowa