OTTER

OTTER (Organized Techniques for Theorem-proving and Effective Research)

• el usuario especifica
  1. los hechos importantes del dominio: conjunto de apoyo (sos)
  2. conocimiento sobre el problema: axiomas de utilidad
  3. ecuaciones de reescritura o demoduladores
  4. parámetros y cláusulas que definen la estrategia de control
• resolución continua de un elemento de sos con un axioma de utilidad
• generalización de la estrategia de cláusula unitaria