Acyclic Programs (Extended Abstract)
Krzysztof Rafal Apt, Marc Bezem · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1990
We study here a natural subclass of the locally stratified programs which we call acyclic.Acyclic programs enjoy several natural properties.First, they exhibit good termination behaviour with respect to a large and natural class of general goals, so they could be used as terminating PROLOG programs.Next, their semantics can be defined in several equivalent ways.In particular we show that the Immediate consequence operator of an acyclic program P has a unique fixpoint Mp, which coincides with the perfect model of P, is the unique Herbrand model of the completion of P and can be identified with the unique fixpcint of the 3valued immediate consequence operator associated with P. The completion of an acyclic program P is shown to satisfy an even stronger property: addition of a domain closure axiom results In a theory which is complete and decidable with respect to a large class of formulas including the variable-free ones.This implies that Mp is recursive.On the procedural side we show that SLS-resolution and SLDNF-resolutlon for acyclic programs coincide, are effective, sound and (non-floundering) complete with respect to the declarative semantics.Finally, we show that various forms of temporal reasoning, as exemplified by the so-called Yale Shooting Problem, can be naturally described by means of acyclic programs.