Please use this identifier to cite or link to this item: https://doi.org/10.1109/69.298170
Title: First-order logic characterization of program properties
Authors: Wang, Ke 
Yuan, Li Yan
Issue Date: Aug-1994
Citation: Wang, Ke,Yuan, Li Yan (1994-08). First-order logic characterization of program properties. IEEE Transactions on Knowledge and Data Engineering 6 (4) : 518-533. ScholarBank@NUS Repository. https://doi.org/10.1109/69.298170
Abstract: A program is first-order reducible (FO-reducible) w.r.t. a set IC of integrity constraints if there exists a first-order theory T such that the set of models for T is exactly the set of intended models for the program w.r.t. all possible EDB's. In this case, we say that P is FO-reducible to T w.r.t. IC. For FO-reducible programs, it is possible to characterize, using first-order logic implications, properties of programs that are related to all possible EDB's as in the database context. These properties include, among others, containment of programs, independence of updates w.r.t. queries and integrity constraints, and characterization and implication of integrity constraints in programs, all of which have no known proof procedures. Therefore, many important problems formalized in a nonstandard logic can be dealt with by using the rich reservoir of first-order theorem-proving tools, provided that the program is FO-reducible. The following classes of programs are shown to be FO-reducible. (1) A stratified acyclic program P is FO-reducible to comp(P)qqIC w.r.t. IC for any set IC of constraints; (2) a general chained program P is FO-reducible to comp(P)qqIC w.r.t. certain acyclicity constraints IC; (3) a bounded program P is FO-reducible to comp(P′)qqIC w.r.t. any set IC of constraints, where P′ is a nonrecursive program equivalent to P. Some heuristics for constructing FO-reducible programs are described.
Source Title: IEEE Transactions on Knowledge and Data Engineering
URI: http://scholarbank.nus.edu.sg/handle/10635/99294
ISSN: 10414347
DOI: 10.1109/69.298170
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

5
checked on Nov 15, 2018

Page view(s)

27
checked on Nov 2, 2018

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.