This Festschrift volume is published in memory of William W. McCune (1953-2011). While he was an accomplished computer scientist all around, Bill McCune was especially a fantastic system builder: his theorem provers Otter and EQP, with which he proved the famous Robbins conjecture, won him the Herbrand Award in 2000. The volume includes 13 full papers, presenting research in many aspects of automated reasoning and its applications to mathematics. The covered topics are: strategies, indexing, superposition-based theorem proving, model building, applications of automated reasoning to geometry, algebra, and logic, as well as to program verification, data mining, and computer formalized mathematics.
Automated Reasoning and Mathematics: Essays in Memory of William W. McCune
BONACINA, Maria Paola;
2013-01-01
Abstract
This Festschrift volume is published in memory of William W. McCune (1953-2011). While he was an accomplished computer scientist all around, Bill McCune was especially a fantastic system builder: his theorem provers Otter and EQP, with which he proved the famous Robbins conjecture, won him the Herbrand Award in 2000. The volume includes 13 full papers, presenting research in many aspects of automated reasoning and its applications to mathematics. The covered topics are: strategies, indexing, superposition-based theorem proving, model building, applications of automated reasoning to geometry, algebra, and logic, as well as to program verification, data mining, and computer formalized mathematics.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
