Es ist eine neuere Version 2023W dieser LV im Curriculum Master's programme Computational Mathematics 2023W vorhanden.
Workload
Education level
Study areas
Responsible person
Hours per week
Coordinating university
1,5 ECTS
B3 - Bachelor's programme 3. year
Mathematics
Teimuraz Kutsia
1 hpw
Johannes Kepler University Linz
Detailed information
Original study plan
Bachelor's programme Technical Mathematics 2013W
Objectives
Description of the main methods for automated reasoning
Subject
Summary of first order predicate logic; the resolution method;
completeness of
resolution (Herbrand Theorem, semantic trees); refinements of resolution;
the DPLL method for SAT; sequent calculus; the Theorema system.
