A Declarative Alternative To Assert In Logic Programming

The problem with the standard means by which Prolog programs are ex- tended | assert | is that the construct is not semantically well-behaved. A more elegant alternative (adopted, for example, in Prolog) is implication with its intuitionistic meaning, but the assumptions so added to a logic pro- gram are of limited applicability. We propose a new construct rule ,w hich combines the declarative semantics of implication with some of the power of assert. Operationally, rule provides for the extension of the logic pro- gram with results that deductively follow from that program. rule, used in conjunction with higher-order programming techniques such as continuation- passing style, allows the natural and declarative formulation of a whole class of logic programs which previously required assert. Example applications include memoization, partial evaluation combined with reflection, resolution, ML type inference, and explanation-based learning.