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 (非官方移植版) | 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 (非官方移植版) | 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 | [文件列表] |