Prova automática de teoremas (PAT) ou dedução automática (DA) é a prova de teoremas matemáticos por um programa de computador. É atualmente a sub-área mais desenvolvida do raciocínio automatizado (RA).