[  lenny  ] [  squeeze  ] [  sid  ]
[ Source: otter  ]

Package: otter (3.3f-1)

resolution-style theorem prover

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.

Other Packages Related to otter

  • depends
  • recommends
  • suggests
  • dep: libc6 (>= 2.3.5-1) [not armel, i386, ia64]
    GNU C Library: Shared libraries
    also a virtual package provided by libc6-udeb
    dep: libc6 (>= 2.3.6-6) [i386]
    dep: libc6 (>= 2.5-5) [armel]
  • dep: libc6.1 (>= 2.3.5-1) [ia64]
    GNU C Library: Shared libraries
    also a virtual package provided by libc6.1-udeb
  • rec: c-shell
    virtual package provided by csh, tcsh
  • rec: mace2
    program that searches for finite models of first-order statements
  • rec: perl
    Larry Wall's Practical Extraction and Report Language
  • sug: formed
    formula editor for first-order logic formulae

Download otter

Download for all available architectures
Architecture Package Size Installed Size Files
amd64 759.1 kB1784 kB [list of files]
armel 747.1 kB1760 kB [list of files]
hppa 763.1 kB1796 kB [list of files]
i386 743.7 kB1760 kB [list of files]
ia64 843.3 kB2184 kB [list of files]
mips 764.4 kB1924 kB [list of files]
mipsel 765.3 kB1924 kB [list of files]
powerpc 754.1 kB1816 kB [list of files]
s390 754.2 kB1788 kB [list of files]
sparc 742.3 kB1772 kB [list of files]