Index-driven semantics of logic programs
Dmitri Boulanger, Maurice Bruynooghe · Lirias · 1995
An operational semantics is presented. It is aimed at developing a wide class of static analysis frameworks. Each computed answer of a program is assigned an index, with encodes SLD-derivations with this computed answer. This is concisely formalised as a reachable $epsilon$-algebra with the constraint s-model as its domain. This puts together the top-down SLD-resolution and the non-ground bottom-up computation giving rise to a novel approach for computing opeational properties with surjective $epsilon$-homomorphisms as an abstraction. An approximation is a finite homomorphic image of the concrete algebra.