DEF: KV grammatika on Greibachi normaalkujul, kui tema produktsioonid on kujul A→aA1A2…An või A→a (muu on tühi sõne) või kujul S → ε, kui keelde L (G) peab kuuluma ka tühi sõne. Iga KV grammatika on teisendatav Greibachi normaalkujule. T: 1) grammatika peab olema Chomsky nk-l. 2) mitteterminaalid nimetatakse ümber A1-ks, A2-ks jne. 3) produktsioonid asendatakse kujule aA1A2A3… Regulaarsete keelte hulk on KV keelte pärisosahulk. Vaatame kasvõi pumpamise lemmasid: uvjw on lihtsalt uvjwxjy erijuht ehk uvjwjxjy= u(vwx)jy. 13 Taandatud KV grammatikad. Iga KV keele jaoks leidub teda genereeriv taandatud KV grammatika: 1) ε-vaba (puuduvad tühja parema poolega produktsioonid, v.a S → ε, kui ε kuulub sellesse keelde) 2) ei sisalda kasutuid sümboleid ehk mitteterminale, millest ei saa tuletada terminaalseid sõnesid; 3) ei sisalda saavutamatuid sümboleid (mis nkn ei teki ühegi produktsiooni käigus kunagi);
mittevälistav disjunktsioon. Eesti loogikaõpikutes esineb sageli ka traditsioonilist käsitlusviisi, ent tänapäeval on valdavaks muutunud lausearvutusega kokkusobiv käsitlemine, mis võimaldab kergemini koostada lausearvutust sisaldavaid tuletusskeeme. Lausearvutusel põhinev versioon näib üldjuhul olevat intuitsiooniga paremas kooskõlas kui traditsiooniline versioon. Allpool käsitletakse mõlemat versiooni. Lemmasid, mis põhinevad modus ponens’i tüüpi arutlusel ehk jaataval moodusel, nimetatakse konstruktiivseteks lemmadeks või jaatava moodusega lemmadeks. Lemmasid, mis põhinevad modus tollens’i tüüpi arutlusel, nimetatakse destruktiivseteks lemmadeks või eitava moodusega lemmadeks. Ülalpool fikseeritud kokkuleppe kohaselt vaatleme kõiki tingimuslikke väiteid materiaalsete implikatsioonidena. Juhul kui tegemist oli tingivate väidetega, siis seda saab arvesse võtta
mittevälistav disjunktsioon. Eesti loogikaõpikutes esineb sageli ka traditsioonilist käsitlusviisi, ent tänapäeval on valdavaks muutunud lausearvutusega kokkusobiv käsitlemine, mis võimaldab kergemini koostada lausearvutust sisaldavaid tuletusskeeme. Lausearvutusel põhinev versioon näib üldjuhul olevat intuitsiooniga paremas kooskõlas kui traditsiooniline versioon. Allpool käsitletakse mõlemat versiooni. Lemmasid, mis põhinevad modus ponens'i tüüpi arutlusel ehk jaataval moodusel, nimetatakse konstruktiivseteks lemmadeks või jaatava moodusega lemmadeks. Lemmasid, mis põhinevad modus tollens'i tüüpi arutlusel, nimetatakse destruktiivseteks lemmadeks või eitava moodusega lemmadeks. Ülalpool fikseeritud kokkuleppe kohaselt vaatleme kõiki tingimuslikke väiteid materiaalsete implikatsioonidena. Juhul kui tegemist oli tingivate väidetega, siis seda saab arvesse võtta lausete tõlgendamise käigus