A succinct solver for ALFP
Flemming Nielson, Hanne Riis Nielson, Helmut Seidl · 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.