Deductive Synthesis of Programs for Query Answering
In this paper we discuss the application of the deductive-tableau method for program synthesis to the generation of programs for computing the answers to the queries posed to a relational database. The input-output specification for the synthesis is directly extracted from the expressions of relational calculus. The synthesis is then divided into two steps: the first one produces programs implementing the operators of relational algebra in an applicative, side-effect free language; the second one translates the queries expressed in relational calculus into equivalent expressions of relational algebra. The syntheses have been machine checked using the Deductive Tableau System1. The work follows a previous application of the deductive-tableau method to the synthesis of programs for data base transactions and aims at developing a test of practical significance for program synthesis.
KeywordsInput Condition Deductive System Relational Algebra Recursive Call Unary Predicate
Unable to display preview. Download preview PDF.
- R. Burback, S.A. Frazer, H. McGuire, J. Smith, M. Winstandley. Using the Deductive Tableau System. Chariot Software Group, 1990.Google Scholar
- G. Gardarin, P. Valduriez. Relational Databases and Knowledge Bases. Addison Wesley, 1989.Google Scholar
- D. Maier. The theory of relational databases. Computer Science Press, 1983.Google Scholar
- Z. Manna, R. Waldinger. The logical basis for computer programming. Vol. 1: Deductive reasoning. Addison Wesley, 1985.Google Scholar
- Z. Manna, R. Waldinger. The logical basis for computer programming. Vol. 2: Deductive systems. Addison Wesley, 1990.Google Scholar
- J.B. Morris. E-resolution: extension of resolution to include the equality relation. Proceedings of the 1st IJCAI, 1969, 394–402.Google Scholar
- X. Qian. Synthesizing database transactions. Proc. of 16th VLDB Conf., Brisbane, Australia, 1990, 552–565.Google Scholar
- X. Qian. The deductive synthesis of database transactions. Ph.D. dissertation, technical report STAN-CS-89–1291. Dept. of Computer Science, Stanford University, 1989.Google Scholar
- R. Rosati. Sintesi di programmi con il metodo dei tableaux deduttivi per il calcolo della risposta ad una interrogazione ad una base di dati. Tesi di Laurea, Univ. Roma “La Sapienza”, (in Italian ) 1991.Google Scholar
- J. Ullman. Principles of database and knowledge-base systems. Computer Science Press, 1988.Google Scholar