William McCune

Research Professor (guest appointment)
Computer Science Department
School of Engineering
University of New Mexico

Photo, Curriculum Vitae

---

Research Areas

• Automated Deduction: Theory, Methods, Applications
• Foundation Theories and Algebra and Logic
• Formal Methods

---

Current and Recent Projects

• ADAM Workshops
• Prover9 and Mace4
• Semantic Guidance for First-order Provers
• Distributivity in Median Algebras
• Group Theory Single Axioms
• Ivy Proof Checker
• See the Prover9/Mace4 examples for information on other projects

---

Automated Deduction Software

• Prover9 and Mace4: Current systems
• Son of Birdbrain II: Web demo of Prover9 and Mace4
• Otter and Mace2: Previous systems
• EQP: An old AC equational prover

---

Papers

• Web pages associated with papers
• Publication list from my CV
• Errors in my papers
• Slides from selected talks

---

Diversions

• Solving Sudoku Puzzles with Mace4
• Son of Birdbrain II: Web demo of Prover9 and Mace4

---

Miscellany

• Mathematical Structures
• Formal Methods Links
• TPTP Problem Library
• QPQ Deductive Software Repository
• The QED Manifesto