Extensional Higher-Order Logic Programming

2011/06/17 by Angelos Charalambidis, Konstantinos Handjopoulos, Charalambidis, A. +5
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)

paper · pdf · doi:10.48550/arxiv.1106.3457

openalex publication_date 2011/06/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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 procedure which is proven sound and complete with respect to the minimum 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.

Related

• The Intricacies of 3-Valued Extensional Semantics for Higher-Order Logic Programs
• Predicate Specialization for Definitional Higher-order Logic Programs
• A Survey of the Proof-Theoretic Foundations of Logic Programming
• Open Higher-Order Logic (Long Version)
• Higher-Order Constrained Horn Clauses and Refinement Types