This workshop brings together practioners and researchers who are concerned with the development and application of automated reasoning for mathematics. Mathematics is arguably the oldest and most investigated domain of application for automated reasoning, with many successful results. At the same time, automated reasoning has only scratched the tip of the mathematical iceberg, and much progress can be made with new techniques, encodings, and applications. Increasingly, mathematicians working in logic, finite algebras and other domains are turning to automated reasoning to help them develop their theories. Constraint solvers, SAT solvers, and model generators have been used in many mathematical applications in recent years. The ESARM workshop will provide a forum for presentation of results, and interaction between researchers, in this fruitful field. Reasoning in all forms (ATP systems, proof assistants, etc) and all logics (classical, non-classical, all orders, etc) is of interest to the workshop. The workshop will discuss only "really running" systems and applications, and not theoretical ideas that have not yet been translated into working software. The workshop has two main topic areas (in the context of automated solution of mathematical problems):
- Implementation techniques and comparisons
- Combinations of automated reasoning systems
- Inference rules and control strategies
- Implemented and evaluated user interfaces
- Other aspects of systems relevant to the workshop topic
- Encoding of mathematical problems into logic, and decoding of logic solutions into mathematics
- Applications of automated reasoning to mathematical theorem proving and discovery tasks in domains such as finite algebras, discrete mathematics, planar geometry, etc.
- Applications of automated reasoning to mathematical knowledge and mathematical ontology management
- Applications of automated reasoning to mathematical modelling
- Applications of automated reasoning to math-intensive AI techniques
- Experiences with practical applications of automated reasoning in mathematics
- Other aspects of applications relevant to the workshop topic
Additionally, the workshop includes system and application demonstrations. Demonstrations of systems and applications described in paper presentations, and demonstrations of systems and applications without an accompanying paper, are both encouraged.
Participants are expected from several sources:
- Researchers who have developed and implemented successful automated reasoning techniques and systems for mathematics.
- Practioners who have deployed automated reasoning systems in mathematics.
- Users who have already attempted to apply automated reasoning in mathematics, and now wish to learn more.
- Potential users who are interested in learning how automated reasoning may be used in mathematics.
The workshop provides a forum for discussion of the techniques necessary to take automated reasoning from the lab and into the "real world" of mathematics. The workshop will enable the attendees to learn from each others' practical experiences, and will document their state-of-the-art techniques.