Tämä työ käsittelee loogisten lauseiden automaattista generointia. Työssä tutkitaan sitä, miten tiedon kerääntymistä voisi hyödyttää automaattisessa todistamisessa. Työssä luodaan tiedon kerääntymistä varten algoritmi, jonka avulla voidaan generoida kaikki tietyssä normaalimuodossa olevat suljetut ja syntaktisesti korrektit kaavat mielivaltaisessa ensimmäisen kertaluvun predikaattilogiikan kielessä.
Kurt Gödel loi yksinkertaisen numeroinnin ensimmäisen kertaluvun predikaattilogiikan ensimmäisen epätäydellisyyslauseen todistamista vuonna 1931. Gödelin järjestelmässä monia luonnollisia lukuja vastaa syntaktisesti virheellinen kaava. Tässä työssä Gödelin numerointia parannetaan niin, että jokaista numeroa vastaa tietyssä normaalimuodossa oleva suljettu ja syntaktisesti oikea kaava valitussa ensimmäisen kertaluvun predikaattilogiikan kielessä.
Tutkielma rakentuu seuraavasti. Ensimmäinen luku on johdanto. Generointia käsitellään toisessa luvussa. Ensimmäisessä liitteessä on lyhyesti ensimmäisen kertaluvun predikaattilogiikan käsitteitä. Toisessa liitteessä todistetaan käytettyjä teoreemoja.
