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-2007 Workshop
  • Robbins Redux
  • Prover9/Mace4/LADR Updates
• Prover9 and Mace4
• Semantic Guidance for First-order Provers
• Distributivity in Median Algebras
• Group Theory Single Axioms
• Ivy Proof Checker
• ADAM-2006 Workshop
• 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