Automated reasoning
[INGI2264]
[30h + 15h] 5 credits
Teacher(s):
Language: English
Level: Second
Aims
- understand and explain basic technics and theoretical bases used in automated reasoning
- understand and be aware of respective advantages of various types of logics, especially for their use in automated reasoning
- apply wisely technics and methods of automated reasoning
- understand and use current and representative automated reasoning systems
- develop applications using methods of automated reasoning
Main themes
- Reasoning based on propositional logic: model generatin, Davis Putnam, ...
- Reasoning based on classicalk logic: resolution, array methods, ...
- Reasoning with equality theory: paramodulation, unification, rewriting, ...
- Reaoning based on induction
- Reaonsing based on non classical logics: typed logic, high-order logics, matching, non-monotonic logic, multivalued logic, temporal logic, ...
- Current system of automated reasoning: HOLn Isabelle, KIV, PVS, B, Otter, Nuprl, ...
- Applications: modeling and solving of problems using automated reasoning methods
Other information (prerequisite, evaluation (assessment methods), course materials recommended readings, ...)
INGI21261 Artificial Intelligence : Knowledge and Representation
Reference book
- Kelly, J. (1997), The Essence of Logic. Prentice Hall.
- Alan Robinson , Andrei Voronkov (Editor): Handbook of Automated Reasoning (Vol 1 & 2), MIT Pres, 2001.