Otter and Mace Users
This page contains some of the researchers
and educators who have used the automated deduction systems
Otter
or
Mace.
Maybe this list should be separated into several areas:
 research in mathematics and logic
 other applications
 Otter or Mace as an automatic subsystem
 evaluation of other systems
 education
Let us know
(mccune@mcs.anl.gov)
if we should add, change, or remove entries.
Note: the secondary points are contexts in which
Otter or Mace were used, and not necessaily
the primary research areas of the users.

Zac Ernst, Florida State University
 propositional logics, philosophy

Michael K. Kinyon, Indiana University South Bend
 loops, quasigroups, nonassociative systems

Kenneth Kunen, University of Wisconsin
 nonassociative algebraic systems

Alexander Leitsch, Technische Universität Wien
 Otter as a subsystem for model building and cut elimination

William McCune, Argonne National Laboratory
 applications to problems in abstract algebra and logic
 search methods and software

Norman Megill, Metamath
 quantum logic, ortholattices (Mace user)

Dale Myers, University of Hawaii
 GOAL,
a program for automated reasoning with subgoals

R. Padmanabhan, University of Manitoba
 universal algebra, group theory, algebraic geometry

J. D. Phillips, Wabash College
 loops, quasigroups, nonassociative systems

David A. Plaisted, UNC at Chapel Hill
 comparing resolution to other deduction methods
 educational tool for coursework
 Stephan Schulz, TU Munich and U. Verona
 use in a proof checker for PCL2 proof protocols as generated by
E

Johann Schumann, NASA Ames
 comparison with other provers for use in program synthesis

Matthew Spinks, Monash University
 algebraic and multiplevalued logic

David Stanovský, Charles University in Prague
 linear identities in complex algebras of subalgebras

Mark Stickel, SRI International
 checking proofs found by other programs

Oswaldo Terán, U. de Los Andes (Venezuela)
 organizational simulation and modelling

Tomas Uribe, SRI International
 Evaluation of other systems
 Education

Bob Veroff, University of New Mexico
 applications to problems in abstract algebra and logic
 search methods and proof sketches

Larry Wos, Argonne National Laboratory
 proof simplification and search strategies
 applications to problems in abstract algebra and logic

Jian Zhang, Chinese Academy of Sciences
 finding finite models of firstorder theories