Category:Automated theorem proving

• Automated theorem proving

A

• Anti-unification
• Automated reasoning

B

• Burrows–Abadi–Needham logic

C

• Chaff algorithm
• Computer-assisted proof
• Concolic testing

D

• Davis–Putnam algorithm
• DPLL algorithm
• DPLL(T)

F

• F* (programming language)
• Fresh variable

G

• Harald Ganzinger
• Geometry Expert

H

• Hilbert system

I

• IsaPlanner

L

• LowerUnits

M

• Method of analytic tableaux
• Model elimination

N

• Non-surveyable proof
• Nuprl

O

• Occurs check

P

• POPLmark challenge
• Proof (truth)
• Proof assistant
• Proof complexity
• Propositional proof system

R

• Reasoning system
• Resolution (logic)
• Rippling

S

• Sequent calculus
• Substitution (logic)
• Geoff Sutcliffe
• System on TPTP

T

• Interactive Theorem Proving (conference)
• Thousands of Problems for Theorem Provers

U

• Unification (computer science)
• Unit propagation

W

• WalkSAT