A Transformational Semantics of Static Embedded Implications of Normal Logic Programs

  • Edelmira Pasarella
  • Fernando Orejas
  • Elvira Pino
  • Marisa Navarro
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3901)


There are mainly two approaches for structuring logic programs. The first one is based on defining some notion of program unit or module and on providing a number of composition operators. The second approach consists in enriching logic programming with a mechanism of abstraction and scoping rules that are frequently found, for instance, in procedural programming. More precisely, this approach has been advocated by Miller and others using implications embedded in the goals of the given program as a structuring mechanism. However, as Giordano, Martelli and Rossi pointed out, we can associate two different visibility rules (static and dynamic) to this kind of structuring mechanism where, obviously, the semantics of the given program depends on the chosen rule.

In this paper we consider normal constraint logic programs (with constructive negation á la Drabent as operational semantics) extended with embedded implications with a static visibility rule. This class of programs combines the expressive power of normal programs with the capability to organize and to enhance dinamically their sets of clauses. In particular, first, we introduce an operational semantics based on constructive negation for this class of programs, taking into account the static visibility rule. Then, we present an alternative semantics in terms of a transformation of the given structured program into a flat one. Finally, we prove the adequacy of this transformation by showing that it preserves the computed answers of the given program. Obviously, this transformation semantics can be used as the basis for an implementation of this structuring mechanism.


Logic Program Composition Operator Logic Programming Operational Semantic Intuitionistic Logic 
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.
    Arruabarrena, R., Navarro, M.: On extended logic language supporting program structuring. In: Proc. of the Joint Conference on Declarative Programming, APPIA-GULP-PRODE 1996, pp. 191–203 (1996)Google Scholar
  2. 2.
    Arruabarrena, R., Lucio, P., Navarro, M.: A Strong Logic Programming View for Static Embedded Implications. In: Thomas, W. (ed.) ETAPS 1999 and FOSSACS 1999. LNCS, vol. 1578, pp. 56–72. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Baldoni, M., Giordano, L., Martelli, A.: Translating a modal Language with embedded implication into Horn clause logic. In: Herre, H., Dyckhoff, R., Schroeder-Heister, P. (eds.) ELP 1996. LNCS, vol. 1050, pp. 19–33. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  4. 4.
    Bonner, A.J., McCarty, L.T.: Adding negation-as-failure to intuitionistic logic programming. In: Proc. of the North American Conference on Logic Programming, NACLP 1990, pp. 681–703 (1990)Google Scholar
  5. 5.
    Bugliesi, M., Lamma, E., Paola, M.: Modularity in logic programming. Journal of Logic Programming 19(20), 443–502 (1994)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Drabent, W.: What is a failure? An approach to constructive negation. Acta Informática 32, 27–59 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Gabbay, M.: N–PROLOG: An extension of Prolog with hypothetical implications II. Logical foundations and negation as failure. Journal of Logic Programming 1(4), 251–283 (1985)CrossRefzbMATHGoogle Scholar
  8. 8.
    Gabbay, M., Reyle, U.: N–PROLOG: An extension of Prolog with hypothetical implications. I. Journal of Logic Programming 1(4), 319–355 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Giordano, L., Martelli, A., Rossi, G.: Extending Horn clause logic with implication goals. Theoretical Computer Science 95(1), 43–74 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Giordano, L., Martelli, A.: Structuring Logic Programs: A Modal Approach. Journal of Logic Programming 21, 59–94 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Giordano, L., Olivetti, N.: Combining negation as failure and embedded implication in logic programs. Journal of Logic Programming 36, 91–147 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Lucio, P.: Structured sequent calculi for combining intuitionistic and classical first-order logic. In: Kirchner, H. (ed.) FroCos 2000. LNCS, vol. 1794, pp. 88–104. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  13. 13.
    McCarty, L.T.: Clausal intuitionistic logic I. Fixed point semantics. Journal of Logic Programming 5, 1–31 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    McCarty, L.T.: Clausal intuitionistic logic II. Tableau proof procedures. Journal of Logic Programming 5, 93–132 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Miller, D.: A logical analysis of modules in logic programming. Journal of Logic Programming 6(1-2), 79–108 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Monteiro, L., Porto, A.: A language for contextual logic programming. In: Logic Programming Languages: constraints, functions and objects, pp. 115–147. MIT Press, Cambridge (1993)Google Scholar
  17. 17.
    Nadathur, G., Miller, D.: Higher–order logic programming. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 5, pp. 499–590. Clarendon Press (1998)Google Scholar
  18. 18.
    Navarro, M.: From modular Horn programs to flat ones: a formal proof for the propositional case. In: Proc. of the Second International Symposium on Innovation in Information and Communication Technology, ISIICT (2004) Technical Report UPV-EHU/ LSI/ TR 01-2004. (2004),
  19. 19.
    Orejas, F., Pasarella, E., Pino, E.: Semantics of normal logic programs with embeddded implications. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, pp. 255–268. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Edelmira Pasarella
    • 1
  • Fernando Orejas
    • 1
  • Elvira Pino
    • 1
  • Marisa Navarro
    • 2
  1. 1.Dpto de L.S.I.Universitat Politècnica de CatalunyaBarcelonaSpain
  2. 2.Dpto de L.S.I.Universidad del País VascoSan SebastiánSpain

Personalised recommendations