Angelos Charalambidis
Abstract
We propose a purely extensional semantics for higher-order logic programming. In this semantics program predicates denote sets of ordered tuples, and two predicates are equal iff they are equal as sets. Moreover, every program has a unique minimum Herbrand model which is the greatest lower bound of all Herbrand models of the program and the least fixed-point of an immediate consequence operator. We also propose an SLD-resolution proof system which is proven sound and complete with respect to the minimum Herbrand model semantics. In other words, we provide a purely extensional theoretical framework for higher-order logic programming which generalizes the familiar theory of classical (first-order) logic programming.
Supplemental Material
Available for Download
The proof is given in an electronic appendix, available online in the ACM Digital Library.
- Abramsky, S. and Jung, A. 1994. Domain theory. In Handbook of Logic in Computer Science III, S. Abramsky, D. Gabbay, and T. Maibaum Eds., Clarendon Press. Google Scholar
Digital Library
- Apt, K. R. 1990. Logic programming. In Handbook of Theoretical Computer Science (Vol. B), J. van Leeuwen Ed., MIT Press, Cambridge, MA, 493--574. Google ScholarDigital Library
- Barendregt, H. P. 1984. The Lambda Calculus: Its Syntax and Semantics. Studies in logic and the foundations of mathematics series, vol. 103, North-Holland.Google Scholar
- Benzmüller, C., Brown, C. E., and Kohlhase, M. 2004. Higher-order semantics and extensionality. J. Symb. Logic 69, 4, 1027--1088.Google ScholarCross Ref
- Bezem, M. 1999. Extensionality of simply typed logic programs. In Proceedings of the International Conference on Logic Programming. The MIT Press, 395--410. Google ScholarDigital Library
- Bezem, M. 2001. An improved extensionality criterion for higher-order logic programs. In Proceedings of the 15th International Workshop on Computer Science Logic. Springer, 203--216. Google ScholarDigital Library
- Birkhoff, G. 1967. Lattice Theory. American Mathematical Society.Google Scholar
- Chen, W., Kifer, M., and Warren, D. 1989. Hilog as a platform for database languages. IEEE Data Eng. Bull. 12, 3, 37--44. Google ScholarDigital Library
- Chen, W., Kifer, M., and Warren, D. S. 1993. Hilog: A foundation for higher-order logic programming. J. Logic Program. 15, 3, 187--230. Google ScholarDigital Library
- Clark, K. L. 1979. Predicate logic as a computational formalism. Res. rep. DOC 79/59. Department of Computing, Imperial College.Google Scholar
- Dowty, D., Wall, R., and Peters, S. 1981. Introduction to Montague Semantics. Studies in Linguistics and Philosophy, Kluwer Academic Publishers.Google Scholar
- Field, A. and Harrison, P. 1988. Functional Programming. International Computer Science Series, Addison-Wesley.Google Scholar
- Grätzer, G. 1978. General Lattice Theory. Academic Press.Google Scholar
- Hill, R. 1974. LUSH-resolution and its completeness. DCL memo 78, Department of Artificial Intelligence, University of Edinburgh.Google Scholar
- Kleene, S. 1959. Countable functionals. In Constructivity in Mathematics, A. Heyting Ed., North Holland, 81--100.Google Scholar
- Kountouriotis, V., Rondogiannis, P., and Wadge, W. W. 2005. Extensional higher-order datalog. In Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Short Paper). 1--5.Google Scholar
- Kreisel, G. 1959. Interpretation of analysis by means of functionals of finite type. In Constructivity in Mathematics, A. Heyting Ed., North Holland, 101--128.Google Scholar
- Lloyd, J. W. 1987. Foundations of Logic Programming. Springer. Google ScholarDigital Library
- Miller, D. and Nadathur, G. 1986. Higher-order logic programming. In Proceedings of the 3rd International Conference on Logic Programming. 448--462. Google ScholarDigital Library
- Nadathur, G. 1987. A higher-order logic as the basis for logic programming. Ph.D. thesis, University of Pennsylvania. Google ScholarDigital Library
- Nadathur, G. and Miller, D. 1990. Higher-order horn clauses. J. ACM 37, 4, 777--814. Google ScholarDigital Library
- Nadathur, G. and Miller, D. 1998. Higher-order logic programming. In Handbook of Logics for Artificial Intelligence and Logic Programming, Vol. 5, Claredon Press, 499--590.Google Scholar
- Normann, D. 2006. Computing with functionals - computability theory or computer science. Bull. Symb. Logic 12, 1, 43--59.Google ScholarCross Ref
- Rondogiannis, P. and Wadge, W. W. 2005. Minimum model semantics for logic programs with negation-as-failure. ACM Trans. Comput. Logic 6, 2, 441--467. Google ScholarDigital Library
- Stoy, J. E. 1977. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA. Google ScholarDigital Library
- Tennent, R. D. 1991. Semantics of Programming Languages. Prentice-Hall.Google Scholar
- Wadge, W. W. 1991. Higher-order horn logic programming. In Proceedings of the International Symposium on Logic Programming. 289--303.Google Scholar
- Warren, D. H. 1982. Higher-order extensions to prolog: Are they needed? Machine Intell. 10, 441--454.Google Scholar
Index Terms
- Extensional Higher-Order Logic Programming
Recommendations
Extensional Higher-Order Paramodulation in Leo-III
AbstractLeo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with ...
Extensional higher-order logic programming
JELIA'10: Proceedings of the 12th European conference on Logics in artificial intelligenceWe propose a purely extensional semantics for higher-order logic programming. Under this semantics, every program has a unique minimum Herbrand model which is the greatest lower bound of all Herbrand models of the program and the least fixed-point of ...
Constructive negation in extensional higher-order logic programming
KR'14: Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and ReasoningExtensional higher-order logic programming has been recently proposed as an interesting extension of classical logic programming. An important characteristic of the new paradigm is that it preserves all the well-known properties of traditional logic ...
Comments