Checking Proofs

Checking proofs

If it cannot be checked, then it is not a proof! If it doesn't generate proofs, then it's not a prover! Bliksem only partially obeys this principle, since it has no way of checking the clause form transformation. However the resolution derivations themselves can be converted into type theory and checked. The programs for doing this are all written in Eclipse Prolog, but there should be no problems running them with other Prolog dialects. The dialect dependent constructions (for filehandling only) are marked by the dialect(X)-predicate. The theoretical foundations for are based on joint work with Marc Bezem and Dimitri Hendriks .

Other links: