This is the command otter that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
PROGRAM:
NAME
otter - resolution-style theorem prover
SYNOPSIS
otter < input-file > output-file
DESCRIPTION
This manual page documents briefly the otter command.
otter is a resolution-style theorem-proving program for first-order logic with equality.
otter includes the inference rules binary resolution, hyperresolution, UR-resolution, and
binary paramodulation. Some of its other abilities and features are conversion from first-
order formulas to clauses, forward and back subsumption, factoring, weighting, answer
literals, term ordering, forward and back demodulation, evaluable functions and
predicates, Knuth-Bendix completion, and the hints strategy.
OPTIONS
No command-line options are accepted; all options are given in the input file.
Use otter online using onworks.net services
