Formulele sunt scrise în logica predicatelor. Sintactic, ele respectă standardul SMT-LIB 2.0 (care include și teorii formalizând aritmetica cu întregi, reali, etc), cu unele extensii specifice. Formulele pot fi introduse interactiv direct în pagina indicată.
O descriere în formatul SMT-LIB e o secvență de s-expresii (liste ierarhice, un format introdus de limbajul LISP), adică fie un atom (cuvânt, în cazul nostru identificator sau operator), fie o listă de expresii într-o paranteze ( ).
Vom începe prin a declara universul U al valorilor:
(declare-sort U)Se poate lucra cu mai multe sorturi (tipuri) disjuncte de valori, dar, la fel ca în logica propozițională clasică vom folosi unul singur.
Predicatele și funcțiile se declară in același mod:
(declare-fun nume (lista-tipuri-argumente) tip-rezultat)deoarece au aceeași structură sintactică: un nume cu o listă de argumente care pot fi termeni. Cum folosim un singur univers de valori U, toate argumentele vor fi de acest sort (tip). Predicatele au rezultatul de tip Bool, iar funcțiile de tip U. Deobicei, sorturile se scriu cu majusculă, celelalte nume cu litere mici, dar nu e o regulă impusă. De exemplu, (declare-fun f (U U) U) definește o funcție de două argumente, cu valori în același univers.
Expresiile cu operatori se scriu tot ca s-expresii, operatorul fiind primul:
(not expresie), (=> expresie expresie),
(= expresie expresie),
iar and și or pot avea oricâte argumente: (and expr1 expr2 ... exprN).
Și predicatele și funcțiile se scriu în aceeași formă, deci pentru p(f(x), y) vom scrie (p (f x) y) (scrierea ne e deja familiară din ML).
Cuantificatorul universal (resp. existențial) se scrie sub forma (forall ((x U)) expresie) (respectiv exists) ceea ce și declară variabila x pentru a putea fi folosită în expresie. Pentru mai multe variabile scriem (forall ((x U) (y U)) expresie) etc. Vom folosi doar formule închise (fără variabile libere) unde nu sunt necesare alte declarații de variabile.
Formulele de mai sus nu se scriu de sine stătător, ci se specifică cu sintaxa (assert formulă) . Dacă specificăm mai mult aserțiuni înseamnă că dorim ca toate să fie adevărate (ele devin deci legate prin conjuncție).
Realizabilitatea aserțiunilor indicate (deci a formulei rezultante ca și conjuncție) se verifică cu comanda (check-sat). Dacă formula e realizabilă, comanda (get-model) produce un model (un univers și o interpretare a funcțiilor pentru care formula e adevărată).
Mai jos e indicată formalizarea completă a exemplului de la curs cu investitorii și acțiunile (exemplul 9). S-a formalizat negația concluziei pentru a evidenția că negația nu e realizabilă împreună cu ipotezele (formează o contradicție), deci concluzia e adevărată (rezultă din ipoteze).
(declare-sort U) (declare-fun buy (U U) Bool) (declare-fun stock (U) Bool) (declare-fun bond (U) Bool) (declare-fun crashDJ () Bool) (declare-fun gold (U) Bool) (declare-fun falls (U) Bool) (declare-fun raterise () Bool) (declare-fun happy (U) Bool) (assert (forall ((b U)) (exists ((o U)) (and (buy b o) (or (stock o) (bond o)))))) (assert (=> crashDJ (forall ((o U)) (=> (and (stock o) (not (gold o))) (falls o))))) (assert (=> raterise (forall ((o U)) (=> (bond o) (falls o))))) (assert (forall ((b U)) (=> (exists ((o U)) (and (buy b o) (falls o))) (not (happy b))))) (assert (not (=> (and crashDJ raterise) (forall ((b U)) (=> (happy b) (exists ((o U)) (and (buy b o) (stock o) (gold o)))))))) (check-sat)Vezi și două rezolvări pentru problema 10, cu unic univers, si cu trei sorturi diferite, ceea ce nu mai necesită predicate pentru categoriile respective, cuantificarea se face deja pe domeniul restrâns.