Automated Deduction and its Application to Mathematics (11w2170)

The "Automated Deduction and its Application to Mathematics" workshop will be hosted at The Banff International Research Station.

Can computers do mathematics? If so, what kind of mathematics? Prover9 (developed by William McCune, University of New Mexico) is a first-order theorem prover, It employs, among other algorithms, the famous Knuth-Bendix algorithm, to decide whether or not two words composed of variables and operators can be proved equal as a consequence of a given set of identities or implications satisfied by the operators. Although the general word problem is well known to be unsolvable, this algorithm provides results in many interesting cases. MACE (models and counterexamples) is a companion program - also developed by McCune, that searches for small finite models and counterexamples. As mathematicians, we make conjectures, prove theorems and give counter-examples. During the past 10+ years, the ADAM workshops have shown the huge success made by Prover9-MACE combination in the use of computers to gather evidence in support of proving or disproving specific mathematical assertions. In this workshop, we plan to demonstrate that computers can be a useful, even essential, tool to mathematical research in the areas of algebra (semigroups, groups and rings) and geometry.

The Banff International Research Station for Mathematical Innovation and Discovery (BIRS) is a collaborative Canada-US-Mexico venture that provides an environment for creative interaction as well as the exchange of ideas, knowledge, and methods within the Mathematical Sciences, with related disciplines and with industry. The research station is located at The Banff Centre in Alberta and is supported by Canada's Natural Science and Engineering Research Council (NSERC), the US National Science Foundation (NSF), Alberta's Advanced Education and Technology, and Mexico's Consejo Nacional de Ciencia y Tecnologí255a (CONACYT).