Overview

Ayane is a theorem prover for first-order logic with equality.

Input format

TPTP (CNF, FOF; supports uninterpreted functions and variables; does not yet support types, arithmetic etc.)

Download

Unix
Windows

Links

Github