Approximation fixpoint theory and the well-founded semantics of higher-order logic programs

DOI10.1017/S1471068418000108MaRDI QIDQ4559803zbMATH OpenOpenAlexFDO

Authors Angelos Charalambidis, Panos Rondogiannis, Ioanna Symeonidou

Publication date 4 December 2018

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1804.08335

zbMATH Keywords

approximation fixpoint theoryhigher-order logic programmingnegation in logic programming

Mathematics Subject Classification ID

Logic programming (68N17)

Abstract: We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic functions at all levels of the type hierarchy. We prove that there exists a bijection between such Fitting-monotonic functions and pairs of two-valued-result functions where the first member of the pair is monotone-antimonotone and the second member is antimonotone-monotone. By deriving an extension of consistent approximation fixpoint theory (Denecker et al. 2004) and utilizing the above bijection, we define an iterative procedure that produces for any given higher-order logic program a distinguished extensional model. We demonstrate that this model is actually a minimal one. Moreover, we prove that our construction generalizes the familiar well-founded semantics for classical logic programs, making in this way our proposal an appealing formulation for capturing the well-founded semantics for higher-order logic programs. This paper is under consideration for acceptance in TPLP.

Recommendations

• Minimum model semantics for extensional higher-order logic programming with negation
• The intricacies of three-valued extensional semantics for higher-order logic programs

Cites work

• A fixed point theorem for non-monotonic functions
• Approximation Fixpoint Theory and the Semantics of Logic and Answers Set Programs
• Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning
• Equivalence of two fixed-point semantics for definitional higher-order logic programs
• Fixpoint semantics for logic programming a survey
• scientific article; zbMATH DE number 517039 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• scientific article; zbMATH DE number 233974 (Why is no real title available?)
• Minimum model semantics for extensional higher-order logic programming with negation
• The intricacies of three-valued extensional semantics for higher-order logic programs
• The Semantics of Predicate Logic as a Programming Language
• The well-founded semantics for general logic programs
• Ultimate approximation and its application in nonmonotonic knowledge representation systems

Cited in

(20)

• Approximate well-founded semantics, query answering and generalized normal logic programs over lattices
• Fixpoint semantics for logic programming a survey
• scientific article; zbMATH DE number 1696794 (Why is no real title available?)
• Efficient Approximation of Well-Founded Justification and Well-Founded Domination
• Approximation Fixpoint Theory and the Semantics of Logic and Answers Set Programs
• Minimum model semantics for extensional higher-order logic programming with negation
• scientific article; zbMATH DE number 1824109 (Why is no real title available?)
• scientific article; zbMATH DE number 25193 (Why is no real title available?)
• An effective fixpoint semantics for linear logic programs
• The intricacies of three-valued extensional semantics for higher-order logic programs
• A Step Up in Expressiveness of Decidable Fixpoint Logics
• Equivalence of two fixed-point semantics for definitional higher-order logic programs
• Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory
• The expressive power of higher-order Datalog
• Equivalence of two fixed-point semantics for definitional higher-order logic programs
• Categorical approximation fixpoint theory
• Non-deterministic approximation fixpoint theory and its application in disjunctive logic programming
• Embedding justification theory in approximation fixpoint theory
• Fixpoint semantics for recursive \textsc{shacl}
• Approximation fixpoint theory in Coq. With an application to logic programming

This page was built for publication: Approximation fixpoint theory and the well-founded semantics of higher-order logic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4559803)