Axiomatizations of backtracking

  • Michel Billaud
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 577)


Goal schemes are terms built from a set of variables (representing goals) and the control structures {false, true, or, and} to which we give a sequential à la Prolog interpretation. We study equivalence relations induced by some interesting classes of elementary goals. We prove that, when goals are allowed to produce side-effects, or when they are restricted to have finite behaviours, there are finite complete axiomatizations that can be used to decide the equivalence of goal schemes. We conjecture that there is no such finite axiomatization in the case of general pure requests.


Prolog semantics of programming languages foundations of logic programming depth-first search backtracking equivalence of program schemes algebraic semantics 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    B. Arbab, D.M. Berry, Operational and Denotational Semantics of Prolog, J. Logic Programming 1987, vol. 4, 309–329.Google Scholar
  2. [2]
    M. Billaud, Formalisation des Structures de ContrÔle de Prolog, Thèse de Troisième Cycle, Université de Bordeaux I, 1985.Google Scholar
  3. [3]
    M. Billaud, Prolog Control Structures, a Formalization and its Applications, in: K.Fuchi and M.Nivat, eds., Programming for Future Generation Computers (North-Holland, Amsterdam, 1988) 57–73.Google Scholar
  4. [4]
    M. Billaud, Simple Operational and Denotational Semantics for Prolog with Cut, Theoretical Computer Science 71 (North-Holland, 1990) 193–208.Google Scholar
  5. [5]
    M. Billaud, Une Sémantique Dénotationnelle Simple pour Prolog avec Prédicats d'Entrées-Sorties, in: Proc. GULP'91, 6to Convegno sulla Programmazione Logica, Pisa (1991), 161–175.Google Scholar
  6. [6]
    M. Billaud, Operational and Denotational Semantics for Prolog with Input-Output Predicates, INFORMATICA'91, Grenoble.Google Scholar
  7. [7]
    E. Börger, A logical Operational Semantics of Full Prolog, IBM Technical Report IKBS 117 (1990)Google Scholar
  8. [8]
    S. Burris, H.P. Sankappanavar, A Course in Universal Algebra, Graduate Texts in Mathematics 78 (Springer-Verlag, 1978).Google Scholar
  9. [9]
    B. Courcelle and M. Nivat, Algebraic Families of Interpretations, in: Proc. 17th Symp. on Foundations of Computer Science, Houston (1976) also available as LABORIA report 189.Google Scholar
  10. [10]
    S. Debray and P. Mishra, Denotational and Operational Semantics for Prolog, in: Journal of Logic Programming (1988) vol. 5, 61–91.Google Scholar
  11. [11]
    E. De Vink, Comparative Semantics for Prolog with Cut, Report IR-166, Vrije Universiteit, Amsterdam (1988), also in Science of Computer Programming 1989–90, vol. 13, 239–264, North-Holland.Google Scholar
  12. [12]
    N.D. Jones and H. Mycroft, Stepwise Development of Operational and Denotational Semantics for Prolog, in: Proc. 1984 Internat. Symp. on Logic Programming (1984) 281–288.Google Scholar
  13. [13]
    G. Markowski and B. Rosen, Bases for chain-complete posets, in: Proc. 16th Symp. on Foundations of Computer Science, Berkeley (1975) 34–47.Google Scholar
  14. [14]
    N.D. North, A denotational definition of Prolog, National Physical Laboratory Report DITS 106/88 (1988).Google Scholar
  15. [15]
    S. Rossi, Semantica denotazionale e operazionale per il Prolog (equivalenza e applicazioni), Thesi di Laurea, Università degli Studi di Padova (1990).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Michel Billaud
    • 1
  1. 1.LaBRI - Université Bordeaux ITalence CedexFrance

Personalised recommendations