Otter Automated deduction system Otter is designed to prove theorems stated in first-order logic with equality. 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. Otter is a fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP. Currently, the main application of Otter is research in abstract algebra and formal logic. Otter and its predecessors have been used to answer many open questions in the areas of finite semigroups, ternary Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry. Otter is coded in C and is portable, easy to install, and fast.

Current Version:   3.0.6 License Type:   Public domain

Home Site: http://www-unix.mcs.anl.gov/AR/otter/ Source Code Availability: Yes Available Binary Packages: Debian Package: No RedHat RPM Package: No Other Packages: No Targeted Platforms: UNIX, Macintosh, DOS, MS Windows 95 Software/Hardware Requirements: Otter is coded in C and is portable, easy to install, and fast. It has been used mostly on UNIX systems, but limited versions also run on PCs and Macintoshes.

Other Links: ftp://info.mcs.anl.gov/pub/Otter/ (FTP site) Mailing Lists/USENET News Groups: To join otter-users mailing list, send a message to majordomo@mcs.anl.gov in which the body of the message is "subscribe otter-users" User Comments: None See A Sample Session?

  SAL Home   |   Mathematics   |   Misc