TY - GEN
T1 - A hierarchy of semantics for normal constraint logic programs
AU - Fages, François
AU - Gori, Roberta
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1996.
PY - 1996/1/1
Y1 - 1996/1/1
N2 - The different properties characterizing the operational behavior of logic programs can be organized in a hierarchy of fixpoint semantics related by Galois insertions, having the least Herbrand model as most abstract semantics, and the SLD operational semantics as most concrete semantics. The choice of a semantics in the hierarchy allows to model precisely the program properties of interest while getting rid of useless details of too concrete semantics, which is crucial for the development of efficient program analysis tools. The aim of this paper is to push forward these methods by making them apply to normal (constraint) logic programs, that is full first-order (non Horn) programs. The fixpoint semantics defined by the first author for the rule of constructive negation by pruning is at the center of the hierarchy developed in this paper. We show that that semantics can be obtained by concretization of Kunen’s semantics defined as a fixpoint, taken as the most abstract semantics of the hierarchy, and that by further concretization it leads to a new operational semantics for normal CLP programs. The different observable properties of the program, such as successful derivations, finite failure, set of computed answer constraints, etc. are modeled by precise semantics in the hierarchy.
AB - The different properties characterizing the operational behavior of logic programs can be organized in a hierarchy of fixpoint semantics related by Galois insertions, having the least Herbrand model as most abstract semantics, and the SLD operational semantics as most concrete semantics. The choice of a semantics in the hierarchy allows to model precisely the program properties of interest while getting rid of useless details of too concrete semantics, which is crucial for the development of efficient program analysis tools. The aim of this paper is to push forward these methods by making them apply to normal (constraint) logic programs, that is full first-order (non Horn) programs. The fixpoint semantics defined by the first author for the rule of constructive negation by pruning is at the center of the hierarchy developed in this paper. We show that that semantics can be obtained by concretization of Kunen’s semantics defined as a fixpoint, taken as the most abstract semantics of the hierarchy, and that by further concretization it leads to a new operational semantics for normal CLP programs. The different observable properties of the program, such as successful derivations, finite failure, set of computed answer constraints, etc. are modeled by precise semantics in the hierarchy.
UR - https://www.scopus.com/pages/publications/84958756079
U2 - 10.1007/3-540-61735-3_5
DO - 10.1007/3-540-61735-3_5
M3 - Conference contribution
AN - SCOPUS:84958756079
SN - 3540617353
SN - 9783540617358
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 77
EP - 91
BT - Algebraic and Logic Programming - 5th International Conference, ALP 1996, Proceedings
A2 - Hanus, Michael
A2 - Rodriguez-Artalejo, Mario
PB - Springer Verlag
T2 - 5th International Conference on Algebraic and Logic Programming, ALP 1996
Y2 - 25 September 1996 through 27 September 1996
ER -