Artificial intelligence in theorem proving 1000-2M19SID
1. Artificial intelligence problems in interactive theorem provers
2. Selection of relevant premises using classical machine learning methods
3. Deep neural networks in theorem proving
4. Calculi used in automated reasoning and their practical properties
5. Proof state evaluation in various calculi
6. Internal proof guidance
7. Reinforcement learning in theorem proving
8. Proof features based on semantic properties and logical models
9. Generative methods in theorem proving
Type of course
Learning outcomes
Knowledge:
1. Artificial intelligence problems in theorem proving
2. Classical machine learning methods in automated reasoning
3. Knowledge of the basic automated theorem proving calculi
4. Characterization of interactive and automated proofs
Skills: The student is able to propose and apply appropriate artificial intelligence methods to a theorem proving problem.
Competences: The student understands the need to adapt existing artificial intelligence methods to the specifics of theorem proving and is able to perform such adaptations.
Assessment criteria
Egzamin pisemny
Bibliography
A. Alemi et al. DeepMath - Deep Sequence Models for Premise Selection
J. Harrison: Handbook of Practical Logic and Automated Reasoning
D. Selsam et al.: NeuroSAT - Learning a SAT Solver from Single-Bit Supervision
K. Krstovski, D. Blei: Equation Embeddings
Additional information
Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:
- Bachelor's degree, first cycle programme, Computer Science
- Master's degree, second cycle programme, Computer Science
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: