OTTER is an automated theorem prover for equational logic developed at Argonne National Laboratory.
OTTER's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. OTTER can also be used as a symbolic calculator and has an embedded equational programming system.
|
|
|
| Архітектура | Розмір пакунка | Розмір після встановлення | Файли |
|---|---|---|---|
| alpha | 770.5 kB | 1876 kB | [список файлів] |
| amd64 | 759.1 kB | 1784 kB | [список файлів] |
| armel | 747.1 kB | 1760 kB | [список файлів] |
| avr32 (unofficial port) | 750.1 kB | 1724 kB | [список файлів] |
| hppa | 763.1 kB | 1796 kB | [список файлів] |
| hurd-i386 | 742.2 kB | 1760 kB | [список файлів] |
| i386 | 743.7 kB | 1760 kB | [список файлів] |
| ia64 | 843.3 kB | 2184 kB | [список файлів] |
| kfreebsd-amd64 | 762.8 kB | 1506 kB | [список файлів] |
| kfreebsd-i386 | 741.7 kB | 1474 kB | [список файлів] |
| m68k (unofficial port) | 729.8 kB | 1744 kB | [список файлів] |
| mips | 764.4 kB | 1924 kB | [список файлів] |
| mipsel | 765.3 kB | 1924 kB | [список файлів] |
| powerpc | 754.1 kB | 1816 kB | [список файлів] |
| s390 | 754.2 kB | 1788 kB | [список файлів] |
| sparc | 742.3 kB | 1772 kB | [список файлів] |