Otter

Resource type
NLP and IR Software
Description

Automatic detection system to prove theorems stated in first-order logic with equality. It is encoded in ANSI C, is portable, easy to install and fast. Used mostly in Unix systems, although some limited versions work on Windows. Free use without restriction.

Enlace