Deductive Synthesis of Programs for Query Answering

  • Daniele Nardi
  • Riccardo Rosati
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


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.


Input Condition Deductive System Relational Algebra Recursive Call Unary Predicate 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    R. Burback, S.A. Frazer, H. McGuire, J. Smith, M. Winstandley. Using the Deductive Tableau System. Chariot Software Group, 1990.Google Scholar
  2. [2]
    J. Freytag, N. Goodman. On the translation of relational queries into iterative programs. ACM Transactions on Database Systems 14: 1, 1989, pp. 1–27.CrossRefGoogle Scholar
  3. [3]
    G. Gardarin, P. Valduriez. Relational Databases and Knowledge Bases. Addison Wesley, 1989.Google Scholar
  4. [4]
    M. Jarke, J. Koch. Query optimization in Database Systems. ACM Computing Surveys, 16, 2 (June 1984), pp. 111–152.MathSciNetMATHCrossRefGoogle Scholar
  5. [5]
    D. Maier. The theory of relational databases. Computer Science Press, 1983.Google Scholar
  6. [6]
    Z. Manna, R. Waldinger. A deductive approach to program synthesis, ACM Transaction on Programming Languages and Systems, 2: 1980,pp. 90–121.MATHCrossRefGoogle Scholar
  7. [7]
    Z. Manna, R. Waldinger. The logical basis for computer programming. Vol. 1: Deductive reasoning. Addison Wesley, 1985.Google Scholar
  8. [8]
    Z. Manna, R. Waldinger. The logical basis for computer programming. Vol. 2: Deductive systems. Addison Wesley, 1990.Google Scholar
  9. [9]
    J.B. Morris. E-resolution: extension of resolution to include the equality relation. Proceedings of the 1st IJCAI, 1969, 394–402.Google Scholar
  10. [10]
    N.W. Murray. Completely nonclausal theorem proving. Art. Int. 18: pp. 67–85, 1982.MATHCrossRefGoogle Scholar
  11. [11]
    D. Nardi. Formal synthesis of a unification algorithm by the Deductive- Tableau method. Journal of Logic Programming, 1989: 7: pp. 1–43.MathSciNetMATHCrossRefGoogle Scholar
  12. [12]
    X. Qian. Synthesizing database transactions. Proc. of 16th VLDB Conf., Brisbane, Australia, 1990, 552–565.Google Scholar
  13. [13]
    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
  14. [14]
    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
  15. [15]
    J. Ullman. Principles of database and knowledge-base systems. Computer Science Press, 1988.Google Scholar

Copyright information

© Springer-Verlag London 1993

Authors and Affiliations

  • Daniele Nardi
    • 1
  • Riccardo Rosati
    • 1
  1. 1.Dipartimento di Informatica e SistemisticaUniversità di Roma “La Sapienza”RomaItalia

Personalised recommendations