The first theorem prover and model generator for first-order logic with equality from the Argonne group that was widely distributed.
Primary LanguageC
Otter, the original Argonne automated theorem prover based on resolution and paramodulation