Interactive Theorem Proving

- Natural & Formal Sciences -
Mathematics & Logic Dictionary
A methodology for producing formal, machine-checked proofs by combining human guidance with proof-assistant software and tactic languages to construct proof scripts that a verifier accepts.