Correct Reasoning About Logic Programs
The focus of this paper lies on provably correct static analysis of logic programs, in particular on determinacy inference for logic programs containing cut, and on verified implementations thereof. For reasons which hardly need spelling out here, the question of whether a goal is deterministic or not is central in logic programming. In practice, logic programmers often use in-build control mechanisms, like the cut in Prolog, to ensure determinacy of certain goals. Yet, to date methods for inferring determinacy conditions on goals have not addressed this close connection between the cuts in a program and the determinacy of its goals.