Dimostrazione automatica di teoremi: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
m smistamento lavoro sporco e fix vari |
Nessun oggetto della modifica |
||
Riga 1:
{{F|teorie dell'informatica|luglio 2017|}}▼
{{S|teorie dell'informatica}}
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 matematica|dimostrazione]] di [[Teorema|teoremi matematici]] da parte di un [[Programma (informatica)|programma]] per [[computer]].
==Definizione==
▲{{F|informatica|luglio 2017|}}
Le tecniche di computazione automatica di un [[teorema]] consistono nell'applicazione di metodi computazionali alla dimostrazione dei teoremi.
In generale, la procedura è la seguente:
| |||