|
|
|
|
|
Reasoning is a process of drawing logical consequences from the given knowledge. The purpose of automated reasoning is to automatize this process, writing systems that help to solve problems either completely automatically or with some user interaction.
After almost sixty year since the first publications in the 1950s, automated reasoning is a mature field of symbolic computation. Significant progress has been achieved both in its theory and implementations. Nowadays, automated reasoning systems are used for proving mathematical theorems, verifying software and hardware, planning and general problem solving, etc. A well-known success story of the field is the solution of the famous Robbins Problem in algebra by the theorem prover EQP in 1996. What mathematicians could not do for 50 years, a prover did in 8 days. Lately, automated reasoning systems gain increasing popularity in industrial applications to support the production of reliable software. Various model checkers, SAT solvers, and theorem provers have been developed and used for this problem.
The list of currently available automated reasoning systems is quite large. These are theorem provers for first-order logic or its equational fragment (e.g., Vampire, E, SPASS, Prover9, iProver, leanCoP, E-Darwin, ACL2, Waldmeister, etc.), provers for higher-order logic and mathematical assistant systems (e.g., Isabelle, HOL, Coq, Leo, Nuprl, Theorema, LambdaCLAM, etc.), model builders and SAT solvers (e.g., Mace4, Paradox, Boolector, Chaff, PrecoSAT, MiniSAT, CVC3, Barcelogic, SATzilla, etc.), model checkers (e.g., BLAST, PRISM, SPIN, Vereofy, etc.), termination provers (e.g., AProVE, TTT2, μ-Term, etc.) and many other tools.
The lecture is intended to give an overview on the variety of available ARSs. After a general introduction to automated reasoning, the course will be organized as a series of tutorials on various reasoning systems. Each participant is expected to prepare a tutorial on a reasoning system of her or his choice and present it in the class.
There will be no exam. The students will be assessed based on (a) the tutorial they prepare and present, and (b) the participation in the lectures.
Summer Semester 2013.
| Number: | 326.097 |
| Title: | Automated Reasoning Systems |
| Lecturer: | Temur Kutsia |
| Time: | Tuesday, 15:30--17:00 |
| Room: | K 009D |
| Language: | English |
| First meeting: | March 12 |
| Registration: | Via the KUSSS system. |