Linked from

The 16 pages that link to Proof assistant, each with the reason it gives.

• Mathematical proofRelated: These systems can verify formal derivations while changing how proofs are produced.

• Intuitionistic logicRelated: Many proof assistants use constructive type theories rooted in intuitionistic logic.

• Natural deductionRelated: Many proof assistants use natural-deduction-style reasoning or related typed calculi.

• Formal verificationRelated: Verification depends on proof assistants whose kernels and foundations require careful scrutiny.

• Formal proofRelated: Proof assistants make large formal derivations practical to build and verify.

• SoundnessRelated: Its trusted kernel depends on sound inference rules to certify theorems.

• Curry–Howard correspondenceRelated: Proof assistants use typed terms to represent proofs and verify them mechanically.

• IntuitionismRelated: Formal constructive systems can be implemented and checked with proof assistants.

• Computer-assisted proofRelated: It can verify each inference in a computer-assisted proof.

• Program verificationRelated: Large verification efforts rely on tools whose proof rules and trusted foundations must be scrutinized.

• ConstructivismRelated: Proof assistants can enforce constructive foundations and extract programs from proofs.

• Disjunction introductionRelated: Its tactics can apply disjunction introduction to establish a disjunctive goal.

• Automated reasoningRelated: Proof assistants combine automated steps with explicit proof objects that a small kernel can verify.

• Biconditional introductionRelated: Formal proof systems can encode introduction rules as permitted proof steps.