
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
K. Wang, L.Y. Yuan, "FirstOrder Logic Characterization of Program Properties," IEEE Transactions on Knowledge and Data Engineering, vol. 6, no. 4, pp. 518533, August, 1994.  
BibTex  x  
@article{ 10.1109/69.298170, author = {K. Wang and L.Y. Yuan}, title = {FirstOrder Logic Characterization of Program Properties}, journal ={IEEE Transactions on Knowledge and Data Engineering}, volume = {6}, number = {4}, issn = {10414347}, year = {1994}, pages = {518533}, doi = {http://doi.ieeecomputersociety.org/10.1109/69.298170}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Knowledge and Data Engineering TI  FirstOrder Logic Characterization of Program Properties IS  4 SN  10414347 SP518 EP533 EPD  518533 A1  K. Wang, A1  L.Y. Yuan, PY  1994 KW  eductive databases; query processing; formal logic; logic programming; database theory; programming theory; firstorder logic; program properties; order reducible; firstorder theory; FOreducible programs; EDBs; database context; integrity constraints; theoremproving tools; stratified acyclic program; general chained program; bounded program; nonrecursive program; deductive databases; fixed points; logic programs; perfect models; query answering; updates; extensional database; inference rules VL  6 JA  IEEE Transactions on Knowledge and Data Engineering ER   
A program is firstorder reducible (FOreducible) w.r.t. a set IC of integrity constraints if there exists a firstorder 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 EDBs. In this case, we say that P is FOreducible to T w.r.t. IC. For FOreducible programs, it is possible to characterize, using firstorder logic implications, properties of programs that are related to all possible EDBs 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 firstorder theoremproving tools, provided that the program is FOreducible. The following classes of programs are shown to be FOreducible: (1) a stratified acyclic program P is FOreducible to comp(P)/spl cup/IC w.r.t. IC for any set IC of constraints; (2) a general chained program P is FOreducible to comp(P')/spl cup/IC w.r.t. certain acyclicity constraints IC; and (3) a bounded program P is FOreducible to comp(P')/spl cup/IC w.r.t. any set IC of constraints, where P' is a nonrecursive program equivalent to P. Some heuristics for constructing FOreducible programs are described.
[1] K. R. Apt and M. Bezem, "Acyclic programs," inProc. 7th Int. Conf. Logic Programming, 1990, pp. 617633.
[2] K. Apt, H. Blair, and A. Walker, "Towards a Theory of Declarative Knowledge,"Proc. Workshop Foundations Deductive Databases and Logic Programming, Washington D.C., 1988, pp. 546629.
[3] S. Abiteboul and R. Hull, "Data functions, datalog and negation," inProc. ACMSIGMOD Conf., 1988.
[4] A. Aho and J. Ullman, "Universality of data retrieval languages," inProc. 6th ACM Symp: Principles of Programming Languages, San Antonio, TX, Jan. 1979.
[5] J. A. Blakeley, N. Coburn, and P.A. Larson, "Updating derived relations: Detecting irrelevant and autonomously computable updates," inProc. Very Large Data Bases, 1986, pp. 457466.
[6] A. Brodsky and Y. Sagiv, "Inference of monotonicity constraints in Datalog programs," inProc. ACM Symp. Principles of Database Syst., 1989, pp. 190199.
[7] K. L. Clark, "Negation as failure," inLogic and Data Bases, H. Gallaire and J. Minker, Eds. New York: Plenum Press, 1978, pp. 293322.
[8] L. Cavedon, "Continuity, consistency, and completeness properties for logic programs," inProc. 6th Int. Conf. Logic Programming, 1989, pp. 571584.
[9] A. K. Chandra and D. Harel, "Hornclause queries and generalizations,"J. Logic Programming, pp. 115, Nov. 1985.
[10] U. S. Chakravarthy, J. Grant, and J. Minker, "Foundations of semantic query optimization for deductive databases," inProc. Int. Workshop Foundations Deductive Databases Logic Programming, J. Minker, Ed., Aug. 1986.
[11] A. K. Chandra and P. M. Merlin, "Implementation of conjunctive queries in relational databases," inProc. 9th ACM SIGACT Symp. Theory of Computing, pp. 7790.
[12] H. Decker, "Integrity enforcement in deductive databases," inProc. 1st Int. Conf. Expert Database Syst., 1986. pp. 281295.
[13] C. Elkan, "Independence of logic database queries and updates," inProc. ACM Symp. Principles of Database Syst., 1990, pp. 154160.
[14] R. Fagin, "Horn clauses and database dependencies,"J. ACM, vol. 29, no. 3, pp. 952985, Oct. 1982.
[15] M. Gelfond and V. Lifschits, "The stable model semantics for logic programming," inProc. 5th Int. Conf. Symp. Logic Programming, 1989, pp. 10701080.
[16] H. Gallaire and J. Minker,Logic and Data Bases. New York: Plenum, 1978.
[17] A. Van Gelder, "The wellfounded semantics for general logic programs,"J. ACM, vol. 38, pp. 620650, 1991.
[18] I. Guessarian, "Deciding boundedness for uniformly connected Datalog programs," Int. Conf. Database Theory,Lecture Notes in Computer Science, 470, pp. 395405, 1990.
[19] P. Kanellakis and S. Abiteboul, "Deciding bounded recursion in database logic programs,"SIGACT News, vol. 20, pp. 1723, 1989.
[20] A. Klug and R. Price, "Determining view dependencies using tableaux,"ACM Trans. Database Syst., vol. 7, no. 3, pp. 361380, Sept. 1982.
[21] J. W. Lloyd,Foundations of Logic Programming, New York: Springer, 1984.
[22] L. W. Lloyd, E. A. Sonenberg, and R. W. Topor, "Integrity constraint checking in stratified database,"J. Logic Programming, vol. 4, pp. 331343, 1987.
[23] J. McCarthy, "Circumscriptiona form of nonmonotonic reasoning,"Artificial Intell., vol. 13, nos. 12, pp. 2739, 1980.
[24] M. J. Maher, "Equivalence of logic programs," inFoundations of Deductive Databases and Logic Programming, J. Minker, Ed. Los Altos, CA: Morgan Kaufmann, 1988, pp. 243274.
[25] E. Mendelson,Introduction to Mathematical Logic, 3rd ed. Monterey, CA: Wadsworth&Brooks/Cole Advanced Books&Software, 1987.
[26] J. M. Nicolas, "Logic for improving integrity checking in relational databases,"Acta Informatica, vol. 18, no. 3, pp. 227253, 19XX.
[27] J. F. Naughton, "Data independent recursion in deductive databases,"J. Comput. Syst. Sci., vol. 39, pp. 256289, 1989.
[28] J. F. Naughton and Y. Sagiv, "A decidable class of bounded recursions," inProc. 6th ACM Symp. Principles of Database Syst.(San Diego, CA), Mar. 1987, pp. 214226.
[29] T. Przymusinski, "On the semantics of stratified deductive databases and logic programs," inFoundations of Deductive Databases and Logic Programming, J. Minker, Ed. Los Altos, CA: MorganKaufman, 1987.
[30] J. A. Robinson, "A machine oriented logic based on the resolution principle,"J. ACM, vol. 18, pp. 636646, 19XX.
[31] K. A. Ross, "Modular acyclicity and tail recursion in logic programs," inProc. ACM Symp. Principles of Database Syst.1991, pp. 92101.
[32] Y. Sagiv, "Optimizing Datalog program." inFoundations of Deductive Databases and Logic Programming, J. Minker, Ed. Los Altos, CA: Morgan Kaufmann, 1988, pp. 659698.
[33] J. C. Shepherdson, "Negation in logic programming," inProc. Foundations of Deductive Databases and Logic Program. (Washington, DC), 1986, J. Minker, Ed.
[34] O. Shmueli, "Decidability and expressiveness aspects of logic queries," inProc. ACM SIGACTSIGMOD Symp. Principles Database Systems, 1987, pp. 237249.
[35] Y. Sagiv and M. Yannakakis, "Equivalences among relational expressions with the union and difference operators,"J. ACM, vol. 27, pp. 633655, 1980.
[36] R. W. Topor and E. A. Sonenberg, "On domain independent databases." inFoundations of Deductive Databases and Logic Programming. J. Minker, Ed. Los Altos, CA: Morgan Kaufmann, 1988, pp. 217240.
[37] J. D. Ullman,Database and Knowledgebase Systems. Rockville, MD: Computer Science Press, 1988.
[38] M. Y. Vardi, "Decidability and undecidability results for boundedness of linear recursive queries," inProc. ACM Symp. Principles of Database Syst., 1988, pp. 341350.