Automated Development of Fundamental Mathematical Theories - 9780792320210

Autor tutvustab automatiseeritud arutluskäiku ja eriti resolutsiooniteoreemi tõestamist, kasutades ütlust OTTER. Ta esitab von Neumann-Bernays-Godeli hulgateooria uue klausliversiooni ja loetleb üle 400 teoreemi, mis on elementaarhulgateoorias poolautomaatselt tõestatud. Ta esitab poolautomaatse tõestuse, et homomorfismide koostis on homomorfism, lahendades seega väljakutseprobleemi. Järgmisena arendab autor Peano aritmeetikat ja annab rohkem kui 1200 elementaararvuteooria definitsiooni ja teoreemi. Ta esitab osa aritmeetika põhiteoreemi (ainulaadne faktorisatsioon) tõestusest ning annab ja OTTERi genereeritud tõestuse Fermat' teoreemi Euleri üldistuse kohta. Järgmisena arendab ta OTTERis Tarski geomeetriat. Ta saab tõendeid enamiku kirjanduses esinevate väljakutsete kohta ja pakub täiendavaid väljakutseid. Seejärel formaliseerib ta modaalloogikaarvutuse K4, et saada Lobi teoreemi ja Godeli kahe mittetäielikkuse teoreemi väga kõrgetasemelised automatiseeritud tõestused. Lõpuks pakub ta väljakutseülesannetena kolmkümmend üks lahendamata ülesannet elementaararvuteoorias.