research-article

Extensional Higher-Order Logic Programming

Authors:

Angelos Charalambidis,

Konstantinos Handjopoulos,

Panagiotis Rondogiannis,

William W. WadgeAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 14, Issue 3

Article No.: 21, Pages 1 - 40

https://doi.org/10.1145/2499937.2499942

Published: 01 August 2013 Publication History

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.

Supplementary Material

PDF File (a21-charalambidis_appendix.pdf)

The proof is given in an electronic appendix, available online in the ACM Digital Library.

Download
147.86 KB

References

[1]

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.

Digital Library

[2]

Apt, K. R. 1990. Logic programming. In Handbook of Theoretical Computer Science (Vol. B), J. van Leeuwen Ed., MIT Press, Cambridge, MA, 493--574.

Digital Library

[3]

Barendregt, H. P. 1984. The Lambda Calculus: Its Syntax and Semantics. Studies in logic and the foundations of mathematics series, vol. 103, North-Holland.

[4]

Benzmüller, C., Brown, C. E., and Kohlhase, M. 2004. Higher-order semantics and extensionality. J. Symb. Logic 69, 4, 1027--1088.

[5]

Bezem, M. 1999. Extensionality of simply typed logic programs. In Proceedings of the International Conference on Logic Programming. The MIT Press, 395--410.

Digital Library

[6]

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.

Digital Library

[7]

Birkhoff, G. 1967. Lattice Theory. American Mathematical Society.

[8]

Chen, W., Kifer, M., and Warren, D. 1989. Hilog as a platform for database languages. IEEE Data Eng. Bull. 12, 3, 37--44.

Digital Library

[9]

Chen, W., Kifer, M., and Warren, D. S. 1993. Hilog: A foundation for higher-order logic programming. J. Logic Program. 15, 3, 187--230.

Digital Library

[10]

Clark, K. L. 1979. Predicate logic as a computational formalism. Res. rep. DOC 79/59. Department of Computing, Imperial College.

[11]

Dowty, D., Wall, R., and Peters, S. 1981. Introduction to Montague Semantics. Studies in Linguistics and Philosophy, Kluwer Academic Publishers.

[12]

Field, A. and Harrison, P. 1988. Functional Programming. International Computer Science Series, Addison-Wesley.

[13]

Grätzer, G. 1978. General Lattice Theory. Academic Press.

[14]

Hill, R. 1974. LUSH-resolution and its completeness. DCL memo 78, Department of Artificial Intelligence, University of Edinburgh.

[15]

Kleene, S. 1959. Countable functionals. In Constructivity in Mathematics, A. Heyting Ed., North Holland, 81--100.

[16]

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.

[17]

Kreisel, G. 1959. Interpretation of analysis by means of functionals of finite type. In Constructivity in Mathematics, A. Heyting Ed., North Holland, 101--128.

[18]

Lloyd, J. W. 1987. Foundations of Logic Programming. Springer.

Digital Library

[19]

Miller, D. and Nadathur, G. 1986. Higher-order logic programming. In Proceedings of the 3rd International Conference on Logic Programming. 448--462.

Digital Library

[20]

Nadathur, G. 1987. A higher-order logic as the basis for logic programming. Ph.D. thesis, University of Pennsylvania.

Digital Library

[21]

Nadathur, G. and Miller, D. 1990. Higher-order horn clauses. J. ACM 37, 4, 777--814.

Digital Library

[22]

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.

[23]

Normann, D. 2006. Computing with functionals - computability theory or computer science. Bull. Symb. Logic 12, 1, 43--59.

[24]

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.

Digital Library

[25]

Stoy, J. E. 1977. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA.

Digital Library

[26]

Tennent, R. D. 1991. Semantics of Programming Languages. Prentice-Hall.

[27]

Wadge, W. W. 1991. Higher-order horn logic programming. In Proceedings of the International Symposium on Logic Programming. 289--303.

[28]

Warren, D. H. 1982. Higher-order extensions to prolog: Are they needed? Machine Intell. 10, 441--454.

Cited By

Burn TOng LRamsay SWagner DGorla D(2021)Initial limit datalogProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470527(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470527
Ong CWagner DBouyer P(2019)HoCHCProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470200(1-14)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470200
Ong CWagner D(2019)HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS.2019.8785784(1-14)Online publication date: Jul-2019
https://doi.org/10.1109/LICS.2019.8785784
Show More Cited By

Index Terms

Extensional Higher-Order Logic Programming

Recommendations

Extensional Higher-Order Paramodulation in Leo-III
Abstract
Leo-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 intelligence

We 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 Reasoning

Extensional 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 14, Issue 3

August 2013

258 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/2499937

Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 2013

Accepted: 01 October 2012

Revised: 01 July 2012

Received: 01 June 2011

Published in TOCL Volume 14, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Greek national funds
Operational Program Education and Lifelong Learning of the National Strategic Reference Framework (NSRF) - Research Funding Program: Heracleitus II
European Social Fund

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
262
Total Downloads

Downloads (Last 12 months)23
Downloads (Last 6 weeks)3

Reflects downloads up to 28 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Burn TOng LRamsay SWagner DGorla D(2021)Initial limit datalogProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470527(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470527
Ong CWagner DBouyer P(2019)HoCHCProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470200(1-14)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470200
Ong CWagner D(2019)HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS.2019.8785784(1-14)Online publication date: Jul-2019
https://doi.org/10.1109/LICS.2019.8785784
BRY F(2019)In Praise of Impredicativity: A Contribution to the Formalization of Meta-ProgrammingTheory and Practice of Logic Programming10.1017/S1471068419000024(1-48)Online publication date: 25-Feb-2019
https://doi.org/10.1017/S1471068419000024
Tourret SCropper A(2019)SLD-Resolution Reduction of Second-Order Horn FragmentsLogics in Artificial Intelligence10.1007/978-3-030-19570-0_17(259-276)Online publication date: 6-May-2019
https://doi.org/10.1007/978-3-030-19570-0_17
Troumpoukis ACharalambidis A(2019)Predicate Specialization for Definitional Higher-Order Logic ProgramsLogic-Based Program Synthesis and Transformation10.1007/978-3-030-13838-7_8(132-147)Online publication date: 23-Feb-2019
https://doi.org/10.1007/978-3-030-13838-7_8
Rondogiannis PSymeonidou I(2018)The intricacies of three-valued extensional semantics for higher-order logic programsProceedings of the 27th International Joint Conference on Artificial Intelligence10.5555/3304652.3304763(5344-5348)Online publication date: 13-Jul-2018
https://dl.acm.org/doi/10.5555/3304652.3304763
CHARALAMBIDIS ARONDOGIANNIS PSYMEONIDOU I(2018)Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic ProgramsTheory and Practice of Logic Programming10.1017/S147106841800010818:3-4(421-437)Online publication date: 10-Aug-2018
https://doi.org/10.1017/S1471068418000108
Charalambidis ARondogiannis PTroumpoukis A(2018)Higher-order logic programming: An expressive language for representing qualitative preferencesScience of Computer Programming10.1016/j.scico.2017.09.002155(173-197)Online publication date: May-2018
https://doi.org/10.1016/j.scico.2017.09.002
Cathcart Burn TOng CRamsay S(2017)Higher-order constrained horn clauses for verificationProceedings of the ACM on Programming Languages10.1145/31580992:POPL(1-28)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158099
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents