Tuletussüsteem koosneb tuletusreeglitest, teisendusreeglitest ja süntaksireeglitest. Oskussõna tuletussüsteem sünonüümideks (mõnetiste kontekstuaalsete eripäradega) on terminid formaalne aksiomaatiline süsteem; arvutus; tõestussüsteem. Tuletus koosneb 2 tuletussammudest. Üks tuletussamm on mingi konkreetse väite tuletamine eelduste või varem saadud vahetulemuste põhjal. Tuletusreeglid näitavad, mida saab mingi kujuga lausena esitatud väitest (oletusest) või väidetest selles tuletussammus järeldada, milline on sammu tulem. Tuletusreegleid ei tohi kasutada asenduste tegemiseks tuletussammu eeldustes või tulemites, selleks saab kasutada teisendusreegleid ehk asendusreegleid. Teisendusreegel lubab mingi sümboli või valemi asendada teise sümboli või valemiga. Asendusi saab teha ka valemi sees. Nt koolialgebra valemites võib valemi (a + a) asendada sümboliga 2a, lausearvutuses võib valemis (¬A ˅ B) & (A → ¬A ˅ B) iga disjunktsiooni kujul ¬A ˅ B asendada
terminid formaalne aksiomaatiline süsteem; arvutus; tõestussüsteem. Tuletus koosneb 2 tuletussammudest. Üks tuletussamm on mingi konkreetse väite tuletamine eelduste või varem saadud vahetulemuste põhjal. Tuletusreeglid näitavad, mida saab mingi kujuga lausena esitatud väitest (oletusest) või väidetest selles tuletussammus järeldada, milline on sammu tulem. Tuletusreegleid ei tohi kasutada asenduste tegemiseks tuletussammu eeldustes või tulemites, selleks saab kasutada teisendusreegleid ehk asendusreegleid. Teisendusreegel lubab mingi sümboli või valemi asendada teise sümboli või valemiga. Asendusi saab teha ka valemi sees. Nt koolialgebra valemites võib valemi (a + a) asendada sümboliga 2a, lausearvutuses võib valemis (¬A B) & (A ¬A B) iga disjunktsiooni kujul ¬A B asendada
annaabi.ee 
