Flemming Nielson, Helmut Seidl and Hanne Riis Nielson. A Succinct Solver for ALFP. Nord. J. Comput., 9(4):335-372, 2002.
We develop a solver algorithm which allows to efficiently compute the stable model of a very expressive fragment of predicate logic. The succinct formulation of the algorithm is due to the disciplined use of continuations and memoisation. This facilitates giving a precise characterisation of the behaviour of the solver and to develop a complexity calculation which allows to obtain its formal complexity. Practical experiments on a control-flow analysis of the ambient calculus show that the solver frequently performs better than the worst-case complexity estimates.
Download: PDF Reference: Bibtex