Formálny systém prvorádovej aritmetiky (Peanova aritmetika) sa používa na špecifikáciu, implementáciu a verifikáciu programov. Problémy sa riešia na cvičeniach v špecifikačno-verifikačnom systéme CL.

Peanova aritmetika. Tautológie a výrokovologické vyplývanie. Logika s kvantifikátormi Dokázateľnosť a logické vyplývanie. Formálna aritmetika: princíp matematickej indukcie a prvorádová axiomatizácia. Rozšírenia aritmetiky. Odvodené induktívne princípy: úplná matematická indukcia, indukcia s mierou, štrukturálna indukcia.
Korektnosť programov. Základné numerické programy. Binárna aritmetika. Dyadická aritmetika a slovné úlohy. Zoznamy. Základné operácie na zoznamoch. Triedenie zoznamov. Aplikácie zoznamov (konečné množiny). Binárne stromy. Základné operácie na stromoch. Binárne vyhľadávacie stromy. Symbolické výrazy.