Dimostrazione automatica di teoremi: differenze tra le versioni

Mentre le radici della logica formalizzata risalgono a Aristotele, è il periodo tra la fine del XIX e l'inizio del XX secolo che ha visto lo sviluppo della logica moderna e della matematica formalizzata. Il libro [[Begriffsschrift]] (1879) di [[Gottlob Frege]] ha introdotto sia un [[calcolo proposizionale]] completo che una [[Linguaggio del primo ordine|logica dei predicati]] essenzialmente moderna<ref>{{Cita libro|cognome=Frege|nome=Gottlob|titolo=Begriffsschrift|anno=1879|editore=Verlag Louis Neuert|url=http://gallica.bnf.fr/ark:/12148/bpt6k65658c}}</ref>. I suoi [[Die Grundlagen der Arithmetik (Fondamenti di aritmetica)]], pubblicati nel 1884<ref>{{Cita libro|cognome=Frege|nome=Gottlob|titolo=Die Grundlagen der Arithmetik|anno=1884|editore=Wilhelm Kobner|città=Breslau|url=http://www.ac-nancy-metz.fr/enseign/philo/textesph/Frege.pdf|urlmorto=sì|urlarchivio=https://web.archive.org/web/20070610094545/http://www.ac-nancy-metz.fr/enseign/philo/textesph/Frege.pdf|dataarchivio=10 giugno 2007}}</ref>, hanno espresso parti di matematica in logica formale. Questo approccio è stato continuato da [[Bertrand Russell|Russell]] e [[Alfred North Whitehead|Whitehead]] nella loro influente opera [[Principia Mathematica]], pubblicata per la prima volta tra il 1910 e il 1913<ref>{{Cita libro|titolo=Principia Mathematica|url=https://archive.org/details/cu31924001575244|anno=1910–1913|editore=Cambridge University Press|autore=Bertrand Russell|edizione=1st|autore2=Alfred North Whitehead}}</ref> e con una seconda edizione rivista nel 1927<ref>{{Cita libro|titolo=Principia Mathematica|anno=1927|editore=Cambridge University Press|autore=Bertrand Russell|edizione=2nd|autore2=Alfred North Whitehead}}</ref>. Russell e Whitehead pensarono di poter derivare tutte le verità matematiche usando assiomi e regole di inferenza di logica formale, iniziando in linea di principio il processo all'automazione. Nel 1920 [[Thoralf Skolem]] semplificò un precedente risultato di [[Leopold Löwenheim]], portando al teorema di Löwenheim-Skolem e, nel 1930, alla nozione di un [[Universo di Herbrand]] e di [[Interpretazione di Herbrand]] che consentiva di ridurre il soddisfacimento (o meno) delle formule di [[Linguaggio del primo ordine|primo ordine]] (e quindi la validità di un teorema) a più (potenzialmente infiniti) problemi di soddisfacimento in termini proposizionali<ref>{{Cita libro|cognome=Herbrand|nome=Jaques|titolo=Recherches sur la théorie de la démonstration|anno=1930}}</ref>.