Showing 1–2 of 2 results for author: Wadge, W W
-
Extensional Higher-Order Logic Programming
Authors:
A. Charalambidis,
K. Handjopoulos,
P. Rondogiannis,
W. W. Wadge
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. W…
▽ More
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.
△ Less
Submitted 17 June, 2011;
originally announced June 2011.
-
Minimum Model Semantics for Logic Programs with Negation-as-Failure
Authors:
Panos Rondogiannis,
William W. Wadge
Abstract:
We give a purely model-theoretic characterization of the semantics of logic programs with negation-as-failure allowed in clause bodies. In our semantics the meaning of a program is, as in the classical case, the unique minimum model in a program-independent ordering. We use an expanded truth domain that has an uncountable linearly ordered set of truth values between False (the minimum element) a…
▽ More
We give a purely model-theoretic characterization of the semantics of logic programs with negation-as-failure allowed in clause bodies. In our semantics the meaning of a program is, as in the classical case, the unique minimum model in a program-independent ordering. We use an expanded truth domain that has an uncountable linearly ordered set of truth values between False (the minimum element) and True (the maximum), with a Zero element in the middle. The truth values below Zero are ordered like the countable ordinals. The values above Zero have exactly the reverse order. Negation is interpreted as reflection about Zero followed by a step towards Zero; the only truth value that remains unaffected by negation is Zero. We show that every program has a unique minimum model M_P, and that this model can be constructed with a T_P iteration which proceeds through the countable ordinals. Furthermore, we demonstrate that M_P can also be obtained through a model intersection construction which generalizes the well-known model intersection theorem for classical logic programming. Finally, we show that by collapsing the true and false values of the infinite-valued model M_P to (the classical) True and False, we obtain a three-valued model identical to the well-founded one.
△ Less
Submitted 3 June, 2003;
originally announced June 2003.
