Automated reasoning [ LINGI2264 ]

INGI 2261 (Artificial Intelligence), or equivalent foundations in logics and artificial intelligence.

• Automated reasoning
• Reasoning based on propositional logic: model generation, Davis Putnam, ...
• Reasoning based on classical logic: resolution, array methods, ...
• Reasoning with equality theory: paramodulation, unification, rewriting, ...
• Reasoning based on induction 
• Common automated reasoning systems
• Applications: modeling and solving of problems using automated reasoning methods

Students completing successfully this course will be able to

• explain basic technics and theoretical bases used in automated reasoning
• describe respective advantages of various types of logics, especially for their use in automated reasoning
• apply wisely technics and methods of automated reasoning
• use current and representative automated reasoning systems
• develop applications using methods of automated reasoning

Students will have developed skills and operational methodology. In particular, they have developed their ability to:

• gather information about the tools available in one area,
  
• make a clear and comprehensive presentation of a software,
• describe a situation, model and analyze it using an appropriate tool.

Not given in 2013-2014

• Introduction
• Propositional logic
• Binary decision diagrams
• First-order logic
• Alloy Foundations
• Equality
• Maude Foundations
• First-order Theories
• Beyond First-ordre Logic

• No mandatory reference book (Many suggested reference books!)
• Slides and documents online