A Proof Procedure for Functional First Order Logic Programs with Non-Deterministic Lazy Functions and Built-in Predicates

摘要

We present a proof procedure for functional first-order logicprograms. The programs we consider allow first-order goals(including disjunctions, conjunctions, negations, andquantifications on elements of the domain). Atoms are either built-in statements or reduction statements of the form t -> s, meaning that t is reducible to s .Call-time choices are used and thefunctions are non-deterministic and non-strict, which allows touse a form of lazy narrowing for pruning the search space and avoiding divergence insome cases.