INTRODUZIONE A OTTER

Otter è un sistema automatizzato di deduzione progettato per dimostrare teoremi dichiarati in logica del primo ordine con l’operatore di uguaglianza. Le regole di inferenza sono basate sulla risoluzione e la paramodulazione, inoltre Otter include la possibilità di riscrittura e ordinamento di termini, nonché di pesatura, e strategie per dirigere e restringere le ricerche per le dimostrazioni. Otter può anche essere usato come calcolatore simbolico e ha incluso un sistema di programmazione ad equazioni.

Prodotto dalla Argonne National Laboratory è il discendente diretto di AURA, NIUTP e ITP ed è ormai alla quarta generazione. Attualmente, le applicazioni principali di questo sistema sono di ricerca nell’algebra astratta e nella logica formale. Otter e i sui predecessori sono stati usati per rispondere a molte questioni aperte nelle aree dei semigruppi finiti, dell’algebra Booleana ternaria, del calcolo logico, della logica combinatoria, della teoria dei gruppi.