Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
A formalization of programs in first-order logic with a discrete linear order
Lin F. Artificial Intelligence235 (C):1-25,2016.Type:Article
Date Reviewed: May 24 2016

Computer programs are language expressions of computations in terms of both the computer, as their computing agent, and behavior, as the computation they represent. Reasoning about computer programs is difficult because of the different natures of the computers and of the computations they perform. Various programming languages use various logics to express program properties. Reactive and concurrent computations use temporal logics where computations are seen as state transitions.

Procedural languages may use various first-order logics, such as the Hoare logic, which expresses computations’ properties by predicates that remain invariant by the computations performed by program statements. The paper we discuss here uses another approach. Computations expressed by program statements are captured as variable values before and after the computation expressed by those statements, which in fact is the same as is done with temporal logic. However, the author relies on a first-order logic with a discrete linear order to express a program computation as a first-order theory with quantification over natural numbers.

The long-term goal of the research presented in this paper is the development of a translator to map a programming language into the first-order logic. Hence, the author envisions the automatic generation of the axioms defining the first-order theory representing the program computation. The body of the work consists of showing the first-order theories representing the computations encapsulated in various kinds of program statements. The mechanism of mapping a program into a first-order theory is illustrated on some classic algorithms, such as Cohen’s integer division algorithm. When properties of programs during their execution are discussed, the author uses labeled programs, which are very similar to labeled transition systems used by Manna and Pnueli in their book [1]. But there is no reference to this book. It would be interesting to see the relationship between the algebraic theory representing the computation expressed by a program, as discussed in this paper, and the language used by Manna and Pnueli to represent the computations expressed by various transition systems. Since this language was used to express the computation performed by a software system [2], such a relationship would represent a real step toward the translator envisioned by the author.

Reviewer:  T. Rus Review #: CR144442 (1608-0591)
1) Manna, Z.; Pnueli, A. Temporal logic and reactive and concurrent systems: specification. Springer, New York, NY, 1992.
2) Rus, T. Computer-based problem solving process. World Scientific, Singapore, 2015.
Bookmark and Share
 
Logics And Meanings Of Programs (F.3 )
 
 
Logic Programming (I.2.3 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Logics And Meanings Of Programs": Date
 A practical theory of reactive systems: incremental modeling of dynamic behaviors (Texts in Theoretical Computer Science)
Kurki-Suonio R., Springer-Verlag New York, Inc., Secaucus, NJ, 2005.  418, Type: Book (9783540233428)
Apr 18 2006
Handling the valuation of the predicates in a fuzzy model
Genito D., Gerla G., Vignes A. Fuzzy Sets and Systems 186(1): 81-99, 2012. Type: Article
May 29 2012
Proofs and computations
Schwichtenberg H., Wainer S., Cambridge University Press, New York, NY, 2012.  480, Type: Book (978-0-521517-69-0)
Oct 30 2012
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy