Inhalt
[ 404SLOCAURV23 ] VL Automated Reasoning
|
|
|
|
 |
| Workload |
Education level |
Study areas |
Responsible person |
Hours per week |
Coordinating university |
| 4,5 ECTS |
M - Master's programme |
Mathematics |
Teimuraz Kutsia |
3 hpw |
Johannes Kepler University Linz |
|
|
|
| Detailed information |
| Original study plan |
Master's programme Computational Mathematics 2025W |
| Learning Outcomes |
Competences |
| Students get acquainted with automated reasoning techniques and tools, from the point of view both of theoretical foundations and practical application, as well as selected advanced topics.
|
|
| Skills |
Knowledge |
- Translating problems formulated in natural language into a logic form (K2)
- Applying various reasoning techniques to problems formulated in propositional or first-order logic (with equality) (K3,K5)
- Understanding (meta-)theorems and (meta-)proofs about properties of reasoning methods (K2,K4)
- Being able to use automated reasoning systems (K3)
- Understanding principles behind automating/implementing reasoning techniques (K2,K4)
|
Logical foundations; various reasoning methods in propositional and first-order logic with equality (including, e.g., resolution and superposition) and their properties; term orderings; methods for solving equational problems; advanced techniques (e.g., combining reasoning with computation or with learning).
|
|
| Criteria for evaluation |
Amount of knowledge on the basic notions and algorithms. Ability to use the main algorithms and the main tools on simple examples.
|
| Methods |
Presentation and discussion of the material in the classroom, accompanying lecture notes, exercises in the classroom and homeworks, individual presentations by the students.
|
| Language |
English |
| Study material |
Lecture notes, tool presentation on their home page on the internet.
|
| Changing subject? |
No |
| Corresponding lecture |
404LFMTAURV20: VL Automated Reasoning (3 ECTS) + 201SYMRSP1V20: VL Symbolic Computation (1.5 ECTS)
|
|
|
|
| On-site course |
| Maximum number of participants |
- |
| Assignment procedure |
Direct assignment |
|
|
|
