**Mail folder:**Interlingua Mail**Next message:**Walter G. Wilson: "Re: First-Order Programming Theories"**Previous message:**Chris Menzel: "Re: Model vs. World"**Reply:**Walter G. Wilson: "Re: First-Order Programming Theories"

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