sekveñcinis skaičiãvimas, vienas formaliosios sistemos, naudojamos aprašyti logiką, pateikimo būdų. Formaliosios sistemos skirtos formalizuoti ir tirti prasmingus įrodymus konkrečioje logikoje. Sekvencinis skaičiavimas predikatų logikai buvo sukonstruotas 1930 vokiečių logiko G. Gentzeno, todėl sekvenciniai skaičiavimai dažnai vadinamas Gentzeno skaičiavimais. Anksčiau F. L. G. Frege’s ir D. Hilberto sukonstruotų skaičiavimų kiekvienam loginiam ryšiui buvo konstruojama sava aksioma. Šio tipo skaičiavimai teiginių logikos atveju turi tik vieną išvedimo taisyklę, vadinamą modus ponens. Sekvenciniuose skaičiavimuose vietoj aksiomų, atitinkančių kiekvieną loginį ryšį, yra konstruojamos išvedimo taisyklės. Šie skaičiavimai teiginių ir predikatų logikų atveju turi tik vieną trivialią aksiomą ir vadinamąsias struktūrines taisykles. Sekvenciniai skaičiavimai yra labiau algoritmiški ir todėl geriau tinka įrodymui konstruoti automatiškai. Čia vietoj formulių yra nagrinėjamos sekvencijos, t. y. A1, … , An → B1, … , Bm (čia A1, … , An, B1, …, Bm yra bet kokios formulės) pavidalo išraiškos. Formulės, esančios kairėje nagrinėjamos sekvencijos rodyklės pusėje, vadinamos antecedentu, o dešinėje – sukcedentu. Sekvencija yra suprantama kaip implikacija, kurios prielaida yra konjunkcija visų formulių, įeinančių į sekvencijos antecedentą, o išvada yra disjunkcija visų formulių, įeinančių į sekvencijos sukcedentą. G. Gentzenas įrodė, kad formulių, įrodomų Frege’s ir Hilberto skaičiavimu, klasė sutampa su formulių, atitinkančių sekvencijoms, įrodomoms sekvenciniu skaičiavimu, klase. Todėl šie skaičiavimai yra ekvivalentūs. Pagrindinė Gentzeno teorema (teorema apie normalinį įrodymų pavidalą predikatų logikoje) teigia, kad bet kokiai įrodomai sekvencijai S galima sukonstruoti įrodymą, kuriame nėra vadinamosios pjūvio taisyklės taikymų (pjūvio taisyklė yra sekvencinis modus ponens taisyklės atitikmuo). Tai reiškia, kad įrodyme gali atsirasti tik formulių, įeinančių į pradinę sekvenciją, tam tikros dalys, t. y. jų paformulės, ir jokių naujų formulių įrodyme neatsiranda. Šiuo atveju sakoma, kad skaičiavimas turi paformulės savybę. Pasinaudojant šia teorema galima gauti įvairių svarbių tvirtinimų, pavyzdžiui, įrodyti predikatų logikos neprieštaringumą; įrodyti teiginių logikos (tiek klasikinės, tiek intuicionistinės) išsprendžiamumą; įrodyti Herbrand’o teoremą, kuri iš esmės yra konstruktyvi Gödelio pilnumo teoremos predikatų logikai versija. Herbrand’o teorema tvirtina, kad kiekviena predikatų logikos formulė yra įrodoma tada ir tik tada, kai galima sukonstruoti atitinkančią jai tapačiai teisingą teiginių logikos formulę. Remiantis Herbrand’o teorema buvo nustatytas glaudus ryšys tarp sekvencinio ir rezoliucijų skaičiavimų. Pastarasis skaičiavimas yra plačiai naudojamas automatizuojant įrodymų paiešką ir yra loginio programavimo teorinis pagrindas. Sekvenciniai skaičiavimai naudojami ne tik predikatų logikai, bet ir įvairioms neklasikinėms logikoms.
2741