Izutsajetsja vozmoznost avtomatizirovannogo postrojenija matematitseskih teori. Rassmatrivajetsja deduktivnaja sistema, osnovannaja na jazyke logiki predikatov pervogo porjadka. Objektami sistemy javljajutsja matematitseskije vyrazenija ili formuly, kotorye opisyvajut...