[ 201LOSDAURU13 ] UE Automated Reasoning
|
|
|
| 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.
|
| Criteria for evaluation |
Written examination
|
| Language |
English |
| Changing subject? |
No |
|
|
|
| On-site course |
| Maximum number of participants |
25 |
| Assignment procedure |
Direct assignment |
|
