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 | [ファイル一覧] |