Skip to main content
SpringerLink
Log in

Proof-Theoretic and Higher-Order Extensions of Logic Programming

  • Chapter
A 25-Year Perspective on Logic Programming

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6125))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alpuente, M., Sessa, M.I. (eds.): 1995 Joint Conference on Declarative Programming, GULP-PRODE 1995, Marina di Vietri, Italy (1995)

    Google Scholar 

  2. Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. Andreoli, J.-M., Pareschi, R.: Linear objects: Logical processes with built-in inheritance. New Generation Computing 9, 445–473 (1991)

    Article  Google Scholar 

  6. Arcelli, F.: Aspetti di ordine superiore e di metalivello della programmazione logica. PhD thesis, DSI, Universitá di Milano (1991)

    Google Scholar 

  7. Arcelli, F., Formato, F.: Implementing higher-order term-rewriting for program transformation in λProlog. In: Alpuente, Sessa [1], pp. 245–256

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. Bozzano, M., Delzanno, G., Martelli, M.: An effective fixpoint semantics for linear logic programs. Theory Pract. Log. Program. 2(1), 85–122 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  14. Bozzano, M., Delzanno, G., Martelli, M.: Model checking linear logic specifications. TPLP 4(5-6), 573–619 (2004)

    MATH  MathSciNet  Google Scholar 

  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. Bugliesi, M., Delzanno, G., Liquori, L., Martelli, M.: Object calculi in linear logic. J. Log. Comput. 10(1), 75–104 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  17. Bugliesi, M., Lamma, E., Mello, P.: Modularity in logic programming. J. Log. Program. 19/20, 443–502 (1994)

    Google Scholar 

  18. Cervesato, I.: Petri nets and linear logic: a case study for logic programming. In: Alpuente, Sessa [1], pp. 313–320

    Google Scholar 

  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. 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. 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]

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639–688 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Article  MATH  MathSciNet  Google Scholar 

  26. Chirimar, J.L.: Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania (May 1995)

    Google Scholar 

  27. Costantini, S., Lanzarone, G.A.: A metalogic programming language. In: ICLP, pp. 218–233 (1989)

    Google Scholar 

  28. Delzanno, G.: Logic and Object-Oriented Programming in Linear Logic. PhD thesis, Universitá di Pisa (February 1997)

    Google Scholar 

  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. Delzanno, G., Martelli, M.: Proofs as computations in linear logic. Theoretical Computer Science 258(1-2), 269–297 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  31. Dovier, A., Pontelli, E. (eds.): 25 Years of Logic Programming in Italy. LNCS, vol. 6125. Springer, Heidelberg (2010)

    Google Scholar 

  32. Felty, A.P.: Implementing tactics and tacticals in a higher-order logic programming language. J. Autom. Reasoning 11(1), 41–81 (1993)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MATH  MathSciNet  Google Scholar 

  34. Gabbay, D.M., Reyle, U.: N-Prolog: An extension of Prolog with hypothetical implications I. J. Log. Program. 1(4), 319–355 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  37. Giordano, L., Olivetti, N.: Combining negation as failure and embedded implications in logic programs. J. Log. Program. 36(2), 91–147 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  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. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)

    MATH  MathSciNet  Google Scholar 

  40. Harper, R., Licata, D.R.: Mechanizing metatheory in a logical framework. J. Funct. Program. 17(4-5), 613–673 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  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. Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science 410(46) (2009)

    Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  46. Miller, D.: A logical analysis of modules in logic programming. Journal of Logic Programming 6(1-2), 79–108 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  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. Miller, D.: A proposal for modules in λProlog. In: Dyckhoff, R. (ed.) ELP 1993. LNCS (LNAI), vol. 798. Springer, Heidelberg (1994)

    Google Scholar 

  49. Miller, D.: Forum: A multiple-conclusion specification logic. Theoretical Computer Science 165(1), 201–232 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Nadathur, G.: Correspondences between classical, intuitionistic and uniform provability. Theoretical Computer Science 232, 273–298 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Pfenning, F.: Computation and deduction. Unpublished lecture notes, p. 217 (Revised March 2001) (May 1992)

    Google Scholar 

  60. Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier Science Publishers, Amsterdam (1999)

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  63. Schürmann, C.: Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, CMU-CS-00-146 (2000)

    Google Scholar 

  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. 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. Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: Specifying properties of concurrent computations in CLF. Electr. Notes Theor. Comput. Sci. 199, 67–87 (2008)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy

    Alberto Momigliano & Mario Ornaghi

  2. Laboratory for the Foundations of Computer Science, School of Informatics, The University of Edinburgh, Scotland

    Alberto Momigliano

Authors
  1. Alberto Momigliano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mario Ornaghi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dip. di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100, Udine, Italy

    Agostino Dovier

  2. Department of Computer Science, New Mexico State University, P.O. Box 30001, 88003, MSC CS, Las Cruces, NM, USA

    Enrico Pontelli

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Momigliano, A., Ornaghi, M. (2010). Proof-Theoretic and Higher-Order Extensions of Logic Programming. In: Dovier, A., Pontelli, E. (eds) A 25-Year Perspective on Logic Programming. Lecture Notes in Computer Science, vol 6125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14309-0_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14309-0_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14308-3

  • Online ISBN: 978-3-642-14309-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation