Automated Theorem Proving for Prolog Verification

Fred Mesnard, Thierry Marianne, Étienne Payet

LPTP (Logic Program Theorem Prover) is an interactive natural-deduction-based theorem prover for pure Prolog programs with negation as failure, unification with the occurs check, a…