Proof-Theoretic and Higher-Order Extensions of Logic Programming

  • Alberto Momigliano
  • Mario Ornaghi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6125)


We review the Italian contribution to proof-theoretic and higher-order extensions of logic programming; this originated from the realization that Horn clauses lacked standard abstraction mechanisms such as higher-order programming, scoping constructs and forms of information hiding. Those extensions were based on the Deduction and Computation paradigm as formulated in Miller et al’s approach [51], which built logic programming around the notion of focused uniform proofs The Italian contribution has been both foundational and applicative, in terms of language extensions, implementation techniques and usage of the new features to capture various computation models. We argue that the emphasis has now moved to the theory and practice of logical frameworks, carrying with it a better understanding of the foundations of proof search.


Logic Program Logic Programming Operational Semantic Linear Logic Logical Framework 
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.
    Alpuente, M., Sessa, M.I. (eds.): 1995 Joint Conference on Declarative Programming, GULP-PRODE 1995, Marina di Vietri, Italy (1995)Google Scholar
  2. 2.
    Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Andreoli, J.-M., Castagnetti, T., Pareschi, R.: Abstract interpretation of linear logic programming. In: Miller, D. (ed.) Proceedings of the International Logic Programming Symposium, Vancouver, Canada, pp. 295–314. MIT Press, Cambridge (1993)Google Scholar
  4. 4.
    Andreoli, J.-M., Pareschi, R.: LO and behold! Concurrent structured processes. In: Proceedings of OOPSLA 1990, Ottawa, Canada, October 1990, vol. 25(10), pp. 44–56. Published as ACM SIGPLAN Notices (1990)Google Scholar
  5. 5.
    Andreoli, J.-M., Pareschi, R.: Linear objects: Logical processes with built-in inheritance. New Generation Computing 9, 445–473 (1991)CrossRefGoogle Scholar
  6. 6.
    Arcelli, F.: Aspetti di ordine superiore e di metalivello della programmazione logica. PhD thesis, DSI, Universitá di Milano (1991)Google Scholar
  7. 7.
    Arcelli, F., Formato, F.: Implementing higher-order term-rewriting for program transformation in λProlog. In: Alpuente, Sessa [1], pp. 245–256Google Scholar
  8. 8.
    Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 391–397. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  9. 9.
    Baldoni, M., Giordano, L., Martelli, A.: A modal extension of logic programming: Modularity, beliefs and hypothetical reasoning. J. Log. Comput. 8(5), 597–635 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Barbuti, R., Mancarella, P., Pedreschi, D., Turini, F.: A transformational approach to negation in logic programming. Journal of Logic Programming 8, 201–228 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Bossi, A., Meo, M.C.: Theoretical Foundations and Semantics. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming in Italy. LNCS, pp. 15–36. Springer, Heidelberg (2010)Google Scholar
  12. 12.
    Bozzano, M., Delzanno, G., Martelli, M.: On the relations between disjunctive and linear logic programming. Electr. Notes Theor. Comput. Sci. 48 (2001)Google Scholar
  13. 13.
    Bozzano, M., Delzanno, G., Martelli, M.: An effective fixpoint semantics for linear logic programs. Theory Pract. Log. Program. 2(1), 85–122 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Bozzano, M., Delzanno, G., Martelli, M.: Model checking linear logic specifications. TPLP 4(5-6), 573–619 (2004)zbMATHMathSciNetGoogle Scholar
  15. 15.
    Bruscoli, P., Guglielmi, A.: Expressiveness of the abstract logic programming language Forum in planning and concurrency. In: Alpuente, M., Barbuti, R., Ramos, I. (eds.) GULP-PRODE (2), pp. 221–237 (1994)Google Scholar
  16. 16.
    Bugliesi, M., Delzanno, G., Liquori, L., Martelli, M.: Object calculi in linear logic. J. Log. Comput. 10(1), 75–104 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Bugliesi, M., Lamma, E., Mello, P.: Modularity in logic programming. J. Log. Program. 19/20, 443–502 (1994)Google Scholar
  18. 18.
    Cervesato, I.: Petri nets and linear logic: a case study for logic programming. In: Alpuente, Sessa [1], pp. 313–320Google Scholar
  19. 19.
    Cervesato, I.: Proof-theoretic foundation of compilation in logic programming languages. In: Jaffar, J. (ed.) Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming (JICSLP 1998), Manchester, UK, pp. 115–129. MIT Press, Cambridge (1998)Google Scholar
  20. 20.
    Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. In: Herre, H., Dyckhoff, R., Schroeder-Heister, P. (eds.) ELP 1996. LNCS (LNAI), vol. 1050, pp. 67–81. Springer, Heidelberg (1996)Google Scholar
  21. 21.
    Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. Theoretical Computer Science 232(1-2), 133–163 (2000); Extended version of [20]zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Cervesato, I., Pfenning, F.: Linear higher-order pre-unification. In: Winskel, G. (ed.) Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS 1997), Warsaw, Poland, pp. 422–433. IEEE Computer Society Press, Los Alamitos (1997)CrossRefGoogle Scholar
  23. 23.
    Cervesato, I., Pfenning, F.: A linear logical framework. Information and Computation (1998); Special issue with invited papers from LICS 1996, Clarke, E. (ed.)Google Scholar
  24. 24.
    Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639–688 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. J. Autom. Reasoning 40(2-3), 133–177 (2008)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Chirimar, J.L.: Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania (May 1995)Google Scholar
  27. 27.
    Costantini, S., Lanzarone, G.A.: A metalogic programming language. In: ICLP, pp. 218–233 (1989)Google Scholar
  28. 28.
    Delzanno, G.: Logic and Object-Oriented Programming in Linear Logic. PhD thesis, Universitá di Pisa (February 1997)Google Scholar
  29. 29.
    Delzanno, G., Giacobazzi, R., Ranzato, F.: Static Analysis, Abstract Interpretation and Verification in (Constraint Logic) Programming. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming in Italy. LNCS, vol. 6125, pp. 136–158. Springer, Heidelberg (2010)Google Scholar
  30. 30.
    Delzanno, G., Martelli, M.: Proofs as computations in linear logic. Theoretical Computer Science 258(1-2), 269–297 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  31. 31.
    Dovier, A., Pontelli, E. (eds.): 25 Years of Logic Programming in Italy. LNCS, vol. 6125. Springer, Heidelberg (2010)Google Scholar
  32. 32.
    Felty, A.P.: Implementing tactics and tacticals in a higher-order logic programming language. J. Autom. Reasoning 11(1), 41–81 (1993)CrossRefMathSciNetGoogle Scholar
  33. 33.
    Gabbay, D.M.: N-Prolog: An extension of Prolog with hypothetical implication II - logical foundations, and negation as failure. J. Log. Program. 2(4), 251–283 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  34. 34.
    Gabbay, D.M., Reyle, U.: N-Prolog: An extension of Prolog with hypothetical implications I. J. Log. Program. 1(4), 319–355 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  35. 35.
    Gabbrielli, M., Palamidessi, C., Valencia, F.D.: Concurrent and Reactive Constraint Programming. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming in Italy. LNCS, vol. 6125, pp. 231–253. Springer, Heidelberg (2010)Google Scholar
  36. 36.
    Gacek, A.: The Abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154–161. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  37. 37.
    Giordano, L., Olivetti, N.: Combining negation as failure and embedded implications in logic programs. J. Log. Program. 36(2), 91–147 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  38. 38.
    Guglielmi, A.: Abstract Logic Programming in Linear Logic Independence and Causality in a First Order Calculus. PhD thesis, Universitá di Pisa (April 1996)Google Scholar
  39. 39.
    Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)zbMATHMathSciNetGoogle Scholar
  40. 40.
    Harper, R., Licata, D.R.: Mechanizing metatheory in a logical framework. J. Funct. Program. 17(4-5), 613–673 (2007)zbMATHCrossRefMathSciNetGoogle Scholar
  41. 41.
    Hodas, J., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Information and Computation 110(2), 327–365 (1994); A preliminary version appeared in the Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 32–42, Amsterdam, The Netherlands (July 1991)Google Scholar
  42. 42.
    Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science 410(46) (2009)Google Scholar
  43. 43.
    López, P., Pfenning, F., Polakow, J., Watkins, K.: Monadic concurrent linear logic programming. In: Barahona, P., Felty, A.P. (eds.) PPDP, pp. 35–46. ACM, New York (2005)Google Scholar
  44. 44.
    Miller, D.: Lexical scoping as universal quantification. In: Levi, G., Martelli, M. (eds.) Proceedings of the Sixth International Conference on Logic Programming, Lisbon, Portugal, pp. 268–283. MIT Press, Cambridge (1989)Google Scholar
  45. 45.
    Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. In: Schroeder-Heister, P. (ed.) ELP 1989. LNCS (LNAI), vol. 475, pp. 253–281. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  46. 46.
    Miller, D.: A logical analysis of modules in logic programming. Journal of Logic Programming 6(1-2), 79–108 (1989)zbMATHCrossRefMathSciNetGoogle Scholar
  47. 47.
    Miller, D.: Abstractions in logic programming. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 329–359. Academic Press, London (1990)Google Scholar
  48. 48.
    Miller, D.: A proposal for modules in λProlog. In: Dyckhoff, R. (ed.) ELP 1993. LNCS (LNAI), vol. 798. Springer, Heidelberg (1994)Google Scholar
  49. 49.
    Miller, D.: Forum: A multiple-conclusion specification logic. Theoretical Computer Science 165(1), 201–232 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  50. 50.
    Miller, D.: Overview of linear logic programming. In: Ehrhard, T., Girard, J.-Y., Ruet, P., Scott, P. (eds.) Linear Logic in Computer Science. London Mathematical Society Lecture Note, vol. 316, pp. 119–150. Cambridge University Press, Cambridge (2004)CrossRefGoogle Scholar
  51. 51.
    Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51, 125–157 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  52. 52.
    Momigliano, A.: Minimal negation and Hereditary Harrop Formulae. In: Nerode, A., Taitslin, M.A. (eds.) LFCS 1992. LNCS, vol. 620, pp. 326–335. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  53. 53.
    Momigliano, A.: Elimination of negation in a logical framework. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 411–426. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  54. 54.
    Momigliano, A., Ambler, S.: Multi-level meta-reasoning with higher-order abstract syntax. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 375–391. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  55. 55.
    Momigliano, A., Tiu, A.F.: Induction and co-induction in sequent calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 293–308. Springer, Heidelberg (2004)Google Scholar
  56. 56.
    Nadathur, G.: Correspondences between classical, intuitionistic and uniform provability. Theoretical Computer Science 232, 273–298 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  57. 57.
    Nadathur, G.: The metalanguage λProlog and its implementation. In: Kuchen, H., Ueda, K. (eds.) FLOPS 2001. LNCS, vol. 2024, pp. 1–20. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  58. 58.
    Pareschi, R.: Type-Driven Natural Language Analysis. PhD thesis, University of Edinburgh. University of Pennsylvania, Department of Computer and Information Science, Technical Report No. MS-CIS-89-45 (July 1989)Google Scholar
  59. 59.
    Pfenning, F.: Computation and deduction. Unpublished lecture notes, p. 217 (Revised March 2001) (May 1992)Google Scholar
  60. 60.
    Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier Science Publishers, Amsterdam (1999)Google Scholar
  61. 61.
    Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Symposium on Language Design and Implementation, Atlanta, Georgia, June 1988, pp. 199–208 (1988)Google Scholar
  62. 62.
    Pfenning, F., Schürmann, C.: System description: Twelf — A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  63. 63.
    Schürmann, C.: Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, CMU-CS-00-146 (2000)Google Scholar
  64. 64.
    Warren, O.H.D.: Higher-order extensions to Prolog: Are they needed? In: Hayes, J.E., Michie, D., Pao, Y.-H. (eds.) Machine Intelligence, vol. 10, pp. 441–454. Halsted Press (1982)Google Scholar
  65. 65.
    Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework: The propositional fragment. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 355–377. Springer, Heidelberg (2004)Google Scholar
  66. 66.
    Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: Specifying properties of concurrent computations in CLF. Electr. Notes Theor. Comput. Sci. 199, 67–87 (2008)CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Alberto Momigliano
    • 1
    • 2
  • Mario Ornaghi
    • 1
  1. 1.Dipartimento di Scienze dell’InformazioneUniversità degli Studi di MilanoItaly
  2. 2.Laboratory for the Foundations of Computer Science, School of InformaticsThe University of EdinburghScotland

Personalised recommendations