Logicheskie dokazatel'stwa

Issleduütsq sekwencial'nye propozicional'nye wywody. Dlq ätogo wwoditsq original'nyj mehanizm diagramm wywodow, predstawlqüschie soboj nagruzhennye grafy proizwol'noj struktury, i opisywaüschie klassy wywodow. Otnoshenie äkwiwalentnosti wywodow, kak izomorfizma kanonicheskih diagramm, sowpadaet s tradicionnoj äkwiwalentnost'ü, opredelqemoj äkwiwalentnymi preobrazowaniqmi wywodow. Diagrammy pozwolqüt reshit' rqd zadach issledowaniq wywodow: opredelit' nelokal'nye preobrazowaniq, sootwetstwuüschih ustraneniü sechenij, bez sobstwenno ih ustraneniq; opisat' formuly secheniq, ne wywodqschie wywody iz klassa äkwiwalentnosti, i t.p. Sformulirowan klass lokal'nyh sekwencij, harakterizuüschihsq prostymi dokazatel'stwami. S drugoj storony opisany klassy slozhno wywodimyh sekwencij. Pri ätom esli argumentom funkcii slozhnosti wystupaet chislo peremennyh, iz kotoryh postroeny sekwenciq, to pochti wse wywody slozhnye. No esli wystupaet dlina sekwencii, to udalos' postroit' tol'ko odnu posledowatel'nost' nelokal'nyh sekwencij, slozhnost' wywodow kotoryh est' äxponenta ot dliny. Kniga prednaznachena studentam, aspirantam i specialistam, zhelaüschim poznakomit'sq s logicheskimi metodami resheniq zadach.