Automated Reasoning

Recommended Prerequisites

Knowledge of group theory obtained in a first undergraduate course of Algebra.   

Teaching Methods

The teaching/learning process will follow an interactive approach in which students will immediately apply the theory taught in solving exercises of various levels. The results will be discussed immediately. 

Learning Outcomes

This learning unit (LU) aims at providing the fundamental knowledge and competencies regarding the principles, concepts, models and techniques that constitute the area of automated reasoning as applied to abstract algebra, namely, principles of automated reasoning and equational reasoning; modelling of algebra problems for automated reasoning; theorem proving strategies; effective usage of state-of-the-art automated theorem provers and finite model builders.

After completion of this LU, students should be able to:

- Recognise the importance of automated reasoning in contemporary abstract algebra, both in its successes and limitations;

- Identify, classify and integrate the principles, main models, algorithms and techniques of automated reasoning as it is applied to algebra;

- Identify, analyze, categorize and evaluate available automated reasoning software; apply it to problems in quasigroup theory, semigroup theory, etc.

Work Placement(s)

No

Syllabus

1) The foundations of automated reasoning: history and development of the area; inference rules and

equational reasoning; algorithms and implementations; first order versus higher order reasoning;

limitations of the methods; finite counterexample building; areas of algebra in which automated reasoning

has been successfully applied, such as quasigroup theory and lattice theory.

2) Quasigroups and loops: concepts and basic principles.

3) Lattices and order: concepts and basic principles.

4) Major automated theorem provers and counterexample builders; modelling algebra problems for automated reasoning software; advanced proof finding strategies; proof modification and complexity reduction; main references for further study.   

Assessment Methods

Assessment
Exam: 30.0%
Resolution Problems: 35.0%
Research work: 35.0%

Bibliography

  - “Automated Reasoning and Discovery of Missing and Elegant Proofs”, L. Wos and G. W. Pieper, Rinton Press,2003, ISBN:1-58949-023-1

- “Automated Reasoning: Introduction and Applications”, L. Wos, R. Overbeek, E. Lusk and J. Boyle,

- “Handbook of Automated Reasoning”, A. Robinson and A. Voronkov (Ed.), Elsevier, ISBN 978-0-444-50813-3, online edition: http://www.sciencedirect.com/science/book/9780444508133

- “Loop Theory”, A. Drapal, M. Kinyon and P. Vojtechovsky, manuscript.