Dimostrazione automatica di teoremi

Da Wikipedia, l'enciclopedia libera.

La dimostrazione automatica di teoremi (in inglese Automated theorem proving o ATP) o deduzione automatica, è il sottocampo più sviluppato del ragionamento automatico. L'operazione consiste nella dimostrazione di teoremi matematici da parte di un programma per computer.

Voci correlate[modifica | modifica wikitesto]