skaičiãvimas, logikoje – dedukcinė sistema, leidžianti sudaryti loginių objektų aibę naudojant pradinius elementus (aksiomas) ir išvedimo taisykles, kurios aprašo naujų elementų sudarymo būdą iš pradinių ir jau sudarytų. Kiekvieną kartą taikant išvedimo taisykles iš aibės elementų (vadinamų taisyklės prielaidomis) sudaromas naujas elementas (vadinamas taisyklės išvada). Kiekvienas skaičiavimas apibūdinamas alfabetu (dar vadinamu kalba), naudojamu sudaryti nagrinėjamus loginius objektus, ir postulatais (aksiomų ir išvedimo taisyklėmis), dažniausiai nurodoma semantika. Kalba ir postulatai nusako skaičiavimo sintaksę. Taip skaičiavimai leidžia formalizuoti matematines (arba logines) aksiomines teorijas ir tirti tam tikros teorijos prasmingus įrodymus. Pagrindinė skaičiavimo sąvoka yra išvedimas (įrodymas). Nagrinėjamojo skaičiavimo išvedimas apibrėžiamas kaip baigtinė tiesiškai sutvarkyta elementų seka, kai kiekvienas tos sekos narys yra arba aksioma, arba gautas pritaikius išvedimo taisyklę anksčiau sudarytiems sekos nariams. Elementas P vadinamas išvedamu nagrinėjamame skaičiavime, jei galima sudaryti išvedimą, kurio paskutinis narys yra P. Išvedimas yra sudaromas tiesiškai arba orientuoto grafo pavidalu. Skaičiavimai gali būti loginiai (pavyzdžiui, teiginių skaičiavimas, predikatų skaičiavimas, neklasikines logikas atitinkantys skaičiavimai ir panašiai), taikomieji (loginiai matematiniai skaičiavimai), kurių loginę dalį sudaro loginis skaičiavimas, ir specialaus pavidalo skaičiavimai, skirti aprašyti algoritmiškai apskaičiuojamas funkcijas (kanoninis, arba Posto, skaičiavimas, λ skaičiavimas, kurio savybėmis grindžiama programavimo kalba LISP, skaičiavimai, skirti aprašyti formaliąją gramatiką). Vienas pagrindinių reikalavimų bet kokiam skaičiavimui yra jo neprieštaringumas – gali būti sudarytas tik teisingos (nagrinėjamo skaičiavimo semantikoje) formulės išvedimas. Svarbi yra skaičiavimo pilnumo, t. y. kiekvienos teisingos formulės išvedimo egzistavimo, problema. Iš Gödelio teoremos (1931) seka, kad taikomieji skaičiavimai, turintys net menką aritmetikos fragmentą, yra nepilni. Taikomieji skaičiavimai dažniausiai yra nepilni, bet teiginių skaičiavimas ir predikatų skaičiavimas yra pilni. Kitas svarbus klausimas – skaičiavimo išsprendžiamumo, t. y. baigiančio darbą algoritmo, leidžiančio nustatyti, ar tam tikra formulė yra išvedama, egzistavimas. 1936 A. Churchas įrodė, kad net predikatų skaičiavimas yra neišsprendžiamas. Išsprendžiamumo tyrimas leidžia nustatyti įvairias neišsprendžiamas problemas, nagrinėti neišsprendžiamų skaičiavimų išsprendžiamus fragmentus. Aprašant loginį arba taikomąjį skaičiavimą naudojami įvairūs jų pateikimo būdai (tipai). Labiausiai žinomi – Hilberto tipo skaičiavimas, sekvencinis skaičiavimas, natūralioji dedukcija, lentelių metodas, rezoliucijų metodas. Kiekvienas pateikimo būdas turi savo privalumų ir trūkumų. Dauguma šiuolaikinių išvedimo paieškos sistemų remiasi rezoliucijų arba lentelių metodu. Įrodyta, kad išvedamų formulių aibė nepriklauso nuo skaičiavimo pateikimo būdo, tuo grindžiamos nagrinėjamo skaičiavimo semantinės savybės, pavyzdžiui, korektiškumas, pilnumas, išsprendžiamumas ir kita. Skaičiavimo vidinės struktūros įvairius klausimus nagrinėja įrodymų teorija.
2741