methods.Theorem provers are used to construct or check proofs.The lattertask
is easierto implement in a tool, but the formeris more useful.Theorem provers
differin how much the user can direct them in constructing proofs. Model checkers
are a recent class of theorem provers that has extended the practicality of formal