Automated and Interactive Reasoning (Raționament Automat și Interactiv) 2025-2026
- Notare
- Evaluare pe parcurs
- bonus pentru prezența la curs: maxim 10p (1p pentru fiecare curs);
- prezența la laborator: maxim 10p (1p pentru fiecare laborator);
- rezolvarea în timpul laboratorului a fișelor de exerciții: maxim 30p;
- lucrul la proiect în timpul laboratorului: maxim 30p;
- implementarea, replicarea și îmbunătățirea rezultatelor dintr-un articol științific: maxim 30p.
- Reexaminare: maxim 100p (punctajele pentru activitățile de mai sus nu se iau în calcul).
- Nota finală se calculează prin împărțirea punctajului final la 10 și rotunjire la cel mai apropiat întreg mai mic sau egal decât 10.
- Contact
- Curs: Ștefan Ciobâcă - stefan.ciobaca@uaic.ro
Referințe Bibliografice
- Dennis Yurichev, SAT/SMT by Example (PDF) (landing page)
- Interactive Z3 guide
- Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson, and Christoph Wintersteiger, Programming Z3
- Leonardo de Moura: Z3 API in Python
Plan de lucru
SMT Solving: Z3
Interactive Theorem Proving: Lean
AI for Theorem Proving
Materiale
- Săptămâna 1
- Săptămâna 2
- Săptămâna 3
- Săptămâna 4
- Săptămâna 5
- Săptămâna 6
- Săptămâna 7
Deschidere an universitar.
Suport curs: Z3 API in Python
Fișiere curs: t1.py, t2.py, t3.py, t4.py, t5.py, t6.py, t7.py, t1.smt, t1.smt, t3.smt, t4.smt
Fișă de lucru laborator: PDF.
Fișiere curs: tba
Fișă de lucru laborator: tba.
Fișiere curs: curs04.dfy
Fișă de lucru laborator: PDF.
Suport curs: DPLL(T) for SMT (Andrew Reynolds), Part 1 DPLL(T) + Quantified Formulas (Andrew Reynolds), Part 2
Fișă de lucru laborator: PDF.
Suport curs: Functional Programming in Lean (David Thrane Christiansen)
Suport curs: Functional Programming in Lean (David Thrane Christiansen)
Fișiere curs: curs07.lean
Fișă de lucru laborator: PDF.