completeness An automatic prover for tautologies in Metamath This program implements the constructive proof of the Completeness Theorem for propositio