Otter and Mace Users

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 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.

• Peter Baumgartner, MPI Informatik, Saarbrücken
  • educational tool for coursework

• Michael Beeson, San Jose State University
  • Otter-Lambda, extending Otter with lambda calculus
  • several graduate student projects

• Johan G. F. Belinfante, Georgia Tech
  • automated reasoning in set theory

• Maria Paola Bonacina, Università degli Studi di Verona
  • proof checking (part of a program analysis project)
  • educational tool for coursework

• Johan Bos, University of Edinburgh
  • DORIS (Discourse Oriented Representation and Inference System)
  • Books on Computational Semantics

• Robert S. Boyer, UT Austin
  • course in automated reasoning

• Ralph Butler, Middle Tennessee State University
  • course in automated ressoning

• Koen Claessen, Chalmers University of Technology
  • proving properties about functional programs (Otter)
  • evaluating Paradox (Mace)

• Simon Colton, Imperial College London
  • automated theory formation

• Zac Ernst, Florida State University
  • propositional logics, philosophy

• Albert C. Esterline ,
  • course in automated reasoning
  • reasoning about agent behavior

• Branden Fitelson, UC Berkeley
  • propositional logics, philosophy

• Norbert E. Fuchs, University of Zurich
  • Attempto Reasoner (natural language processing)

• Adam Grabowski, University of Bialystok
  • translation of Otter proofs into Mizar

• Paul Haroun, McGill University
  • proof checking and comparison with CARINE

• Sandro Hawke, World Wide Web Consortium (W3C)
  • Surnia, a reasoner for OWL (Web Ontology Language)

• Michael K. Kinyon, Indiana University South Bend
  • loops, quasigroups, non-associative systems

• Kenneth Kunen, University of Wisconsin
  • non-associative algebraic systems

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

• Christopher Lynch, Clarkson University
  • course in artificial intelligence

• Olga Shumsky Matlin, Argonne National Laboratory
  • a verified preprocessor and proof-checker
  • modeling message passing software

• William McCune, University of New Mexico
  • 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

• NABESHIMA Hidetomo,
  • Otter as a benchmark for Solar

• Ed Nelson, Princeton University
  • course in automated reasoning

• Monty Newborn, McGill University
  • analysis of Otter proofs in Automated Theorem Proving: Theory and Practice

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

• Mladen Pavičić, University of Zagreb
  • quantum computing, Quantum Implication Algebras

• Peter Penner, University of Manitoba
  • universal algebra, hyper-identities

• J. D. Phillips, Wabash College
  • loops, quasigroups, non-associative systems

• David A. Plaisted, UNC at Chapel Hill
  • comparing resolution to other deduction methods
  • educational tool for coursework

• Alexandre Riazanov, University of Manchester (UK)
  • Mace through System on TPTP
  • evaluating Vampire Prover

• Renate Schmidt, University of Manchester (UK)
  • SCAN Project (SCAN System)

• 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

• Rolf Schwitter, Macquarie University
  • PENG (natural language processing)

• Jörg Siekmann, Universität des Saarlandes
  • Omega Project (Otter is one of several subsystems)

• John Slaney, Australian National University
  • SCOTT, Semantically Constrained Otter
  • Son of SCOTT

• Rick Sommer, Stanford University
  • Education Program for Gifted Youth (EPGY)
  • EPGY Theorem Proving Environment

• Matthew Spinks, Monash University
  • algebraic and multiple-valued logic

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

• Mark Stickel, SRI International
  • checking proofs found by other programs

• Geoff Sutcliffe, University of Miami
  • evaluation of theorem provers, special-purpose theorem provers
  • System on TPTP

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

• Tomas Uribe, SRI International
  • Evaluation of other systems
  • Education

• Josef Urban, Charles University in Prague
  • Otter2Mizar: Mizar articles from Otter proofs

• J. A. Van der Poll, University of South Africa
  • Automated Support for Enterprise Information Systems

• 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

• Paul Youn, MIT
  • The Analysis of Cryptographic APIs Using The Theorem Prover Otter (M.S. thesis)

• Jian Zhang, Chinese Academy of Sciences
  • finding finite models of first-order theories