Skip to content

Automated Theorem Proving

Public syllabus for 2025-2026

Back to syllabi

Academic overview

Programme
AIDC
Period
Year 1, Semester 2
Credits
6
Weeks
14

Curriculum placement

Appears in study plans

AIDC (2025 - 2027) Year 1, Semester 2 Elective subject, group 2

Teaching team

Course coordinator
Tudor Jebelean
Seminar coordinators
Isabela Drămnesc

Learning time distribution

Total
Curriculum Lecture Practice Total Weekly Lecture Practice
42 28 14 3 2 1
Exam hours
14
Individual Study Bibliography study Field study Homework Tutoring Others
94 33 14 43 4 0
Overall
150

Learning outcomes

Knowledge

  • Cognitive understand the principles of Mathematical Logic and its mathematical models;
  • Study the main proving method in propositional logic and in first order predicate logic;
  • Acquire the skills for using Mathematical Logic in Mathematics and Computer Science;
  • Study the applications of Mathematical Logic to algorithm development and verification.
  • Technical: Perform concrete tasks with (1)-(4) above.
  • Affective cognitive: Understand that the cognitive and technical skills above as important for a computer scientist.
  • (6a03a0952355ae3a04d2f2ed) Advanced knowledge in the field of logic and automated reasoning;

Skills

  • Identify situations in which computational logic techniques and algorithms can play a role in problem solving and apply it.
  • The ability to propose/analyze/demonstrate/develop innovative concepts and theories

Responsibility

  • (6a03a0952355ae3a04d2f300) Continuous professional development in the field of activity;

Online platform

Google Classroom

Course content

Content Methods Obs
C1. Chapter 1. Introduction. Examples relating Logic to Mathematics and Computer Science. Q&A/Lecture/Dialogue 2h
C2. Chapter 1. Introduction. The principles of Mathematical Logic and its role in human activity. Q&A/Lecture/Dialogue 2h
C3. Chapter 2. Propositional Logic. Syntax Q&A/Lecture/Dialogue 2h
C4. Chapter 2. Propositional Logic. Semantics, Semantics based notions. Q&A/Lecture/Dialogue 2h
C5. Chapter 2. Equivalences for transforming formulae, Normal Forms. Q&A/Lecture/Dialogue 2h
C6. Chapter 2. Propositional Logic. Resolution, the DPLL method. Q&A/Lecture/Dialogue 2h
C7. Chapter 2. Propositional Logic. Sequent calculus. Q&A/Lecture/Dialogue 2h
C8. Chapter 3. Predicate Logic. Syntax and semantics. Q&A/Lecture/Dialogue 2h
C9. Chapter 3. Predicate Logic. Equivalences for transforming formulae, Normal Forms. Q&A/Lecture/Dialogue 2h
C10. Chapter 3. Predicate Logic. Resolution. Q&A/Lecture/Dialogue 2h
C11. Chapter 3. Predicate Logic. The Herbrand theorem. Q&A/Lecture/Dialogue 2h
C12. Chapter 3. Predicate Logic. Sequent calculus. Q&A/Lecture/Dialogue 2h
C13. Chapter 3. Predicate Logic. Reasoning with equality. Q&A/Lecture/Dialogue 2h
C14. Chapter 4. Predicate Logic. Logical-based program verification and algorithm synthesis. Q&A/Lecture/Dialogue 2h

Course bibliography

Tudor Jebelean. Automatic Theorem Proving. Lecture Notes (online) Bruno Buchberger. Logic for Computer Science. Lecture Notes (online) Chin-Liang Chang, Richard Char-Tung Leel. Symbolic Logic and Mechanica Theorem Proving. Academic Preess, 1973. Jean Gallier. Logic for Computer Science. Foundations of Automatic Theorem Proving.

Seminar content

Content Methods Obs
Lab 1-7. Exemplification of the concepts introduced in the lectures. Experiment, discussion, team work, homework, small programming projects. Student tasks on Google Classroom
Bibliography:Tudor Jebelean. Automatic Theorem Proving. Lecture Notes (online) Bruno Buchberger. Logic for Computer Science. Lecture Notes (online) Chin-Liang Chang, Richard Char-Tung Leel. Symbolic Logic and Mechanica Theorem Proving. Academic Preess, 1973. Jean Gallier. Logic for Computer Science. Foundations of Automatic Theorem Proving.

Seminar bibliography

The content of the lecture is similar to similar standard lectures in well known and established universities.

Corroboration

(none)

AI tools guidance

The use of GenAI tools is not allowed during the examination.

Evaluation and delivery

Activity Criteria Methods Percentage
C
  • 10: excellent (outstanding performance with only minor errors),
  • 8-9: very good (above the average standard but with some errors),
  • 6-7: satisfactory (fair, but with significant shortcomings),
  • 5: sufficient (performance meets minimum criteria),
  • 0-4: fail (significant work has to be done).
  • Written exam.
  • 70.0%
S
  • Homeworks
  • Homework presentation at the whiteboard; Small programming projects
  • 30.0%

Performance standards

10.6. Minimal knowledge for passing / Standard minim de performanță Minimal (grade 5): general understanding of the material, ability to answer 41% of the material (as the sum of the written exam and seminar/lab tasks).

Additional info

-