|Submission of presentations deadline - 23rd May|
Integrating Symbolic Computation and Mechanised Reasoning
Currently, symbolic computation is divided into several (more or less) independent branches: traditional ones (e.g., computer algebra and mechanised reasoning) as well as newly emerging ones (on user interfaces, knowledge management, theory exploration, etc.) The main concern of the Calculemus community is to bring these developments together in order to facilitate the theory, design, and implementation of integrated systems for computer mathematics that will routinely be used by mathematicians, computer scientists and engineers in their every day business.
The scope of Calculemus covers all aspects of the interplay of mechanised reasoning and computer algebra, including cross-fertilisation between those two research areas, as well as the development of integrated systems that transcend both computer algebra and theorem proving.
Hence, potential areas of interest are:
- Theorem proving in computer algebra (CAS)
- Computer algebra in theorem proving (PA and ATP)
- Case studies and applications that both involve computer algebra and mechanised reasoning
- Representation of mathematics in computer algebra
- Theory, design and implementation of interdisciplinary systems for computer mathematics
- Infrastructure for mathematical services
- Theory exploration techniques
Papers on other topics with links to the above research fields and topics will also be welcomed for