News Archives

[Colloquium] Constraint Satisfaction for First-Order Logic

October 31, 2008

Watch Colloquium: 

Quicktime file (314 Megs)
AVI file (487 Megs)


  • Date: Friday, October 31st, 2008 
  • Time: 2 pm — 3:15 pm 
  • Place: ME 218

William McCune
Department of Computer Science University of New Mexico

Abstract: I will describe the problem of searching for finite models of statements in first-order and equational logic. This is a kind of finite-domain constraint satisfaction. So far, the methods have been used mostly to search for counterexamples to conjectures, serving as a complement to programs that search for proofs. The expressiveness of the language and the power of the methods point to wider applications. The methods will be illustrated by using the Mace4 program on problems in abstract algebra and on several puzzles. The problem of isomorphic solutions will be addressed. Some background on automated deduction in first-order and equational logic will be included.

Bio: William McCune has been working in automated deduction since 1981. He received a Ph.D. in computer science from Northwestern University in 1984 and worked at Argonne National Laboratory from 1984 through 2006, ending his tenure there as a senior computational logician. He was also a senior research fellow at the University of Chicago Computation Institute. He has been a part-time research professor in the UNM CS department since 2007, working on several projects with Prof. Robert Veroff. McCune received a Royal E. Cabell research fellowship in 1984, chaired the International Conference on Automated Deduction in 1997, and received the Herbrand Award for Distinguished Contributions to Automated Deduction in 2000. He is the primary author of the automated deduction systems Otter, EQP, Prover9, and Mace.