Every Formula-Based Logic Program Has a Least Infinite-Valued Model

TL;DR

This paper extends the concept of least models in logic programming to formula-based programs using infinite-valued logics, demonstrating that such programs always have a least infinite-valued model.

Contribution

It generalizes the existence of least models from normal to formula-based logic programs through an infinite-valued semantics approach.

Findings

Every formula-based logic program has a least infinite-valued model.

The constructed interpretation M_P is the least among all models of the program.

Extension of infinite-valued semantics to a broader class of logic programs.

Abstract

Every definite logic program has as its meaning a least Herbrand model with respect to the program-independent ordering "set-inclusion". In the case of normal logic programs there do not exist least models in general. However, according to a recent approach by Rondogiannis and Wadge, who consider infinite-valued models, every normal logic program does have a least model with respect to a program-independent ordering. We show that this approach can be extended to formula-based logic programs (i.e., finite sets of rules of the form A\leftarrowF where A is an atom and F an arbitrary first-order formula). We construct for a given program P an interpretation M_P and show that it is the least of all models of P. Keywords: Logic programming, semantics of programs, negation-as-failure, infinite-valued logics, set theory