You must enable JavaScript to use this site

  • Track A: Calculemus (Chair: James Davenport)

    Calculemus is a series of conferences dedicated to the integration of computer algebra systems (CAS) and systems for mechanised reasoning like interactive proof assistants (PA) or automated theorem provers (ATP). 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 mathematical assistant systems that will be used routinely by mathematicians, computer scientists and all others who need computer-supported mathematics in their every day business.

    The topics of interest of Calculemus include but are not limited to:
    • Automated theorem proving in computer algebra systems.
    • Computer algebra in theorem proving systems.
    • Case studies and applications that involve a mix of computation and reasoning.
    • Representation of mathematics in computer algebra systems.
    • Adding computational capabilities to theorem proving systems.
    • Adding reasoning capabilities to computer algebra systems.
    • Combining methods of symbolic computation and formal deduction.
    • Theory, design and implementation of interdisciplinary systems for computer mathematics.
    • Theory exploration techniques.
    • Case studies in formalization of mathematical theories.
    • Input languages, programming languages, types and constraint languages, and modeling languages for mechanised mathematics systems (PA, CAS, and ATP).
    • Infrastructure for mathematical services.

  • News



    cicm2014 logo
    coimbra logo
Privacy policy and legal information
Last modified: April 04 2018 09:42:19 CEST