otter

resolution-style theorem prover

Install

All systems
curl cmd.cat/otter.sh
Debian Debian
apt-get install otter
Ubuntu
apt-get install otter
Windows (WSL2)
sudo apt-get update sudo apt-get install otter
Raspbian
apt-get install otter

otter

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.