Theorem prover

View project on GitHub

Ayane is a theorem prover for first-order logic with equality, types and limited arithmetic capabilities. It accepts a problem specification in DIMACS or TPTP format and attempts to determine whether the problem is satisfiable or unsatisfiable.

Performance is still a work in progress; the current version of the system can solve only a limited range of problems.


Ayane requires an up-to-date C++ compiler, GMP and Boost. To compile from source:

make CXXFLAGS='-O3 -flto'
make install

(CXXFLAGS is not required, but is recommended as it makes the program run slightly faster.)


A 64-bit executable is provided in the zip file.

The instructions for compiling Ayane on Windows assume Microsoft C++ 2013 is installed, and use the command line compiler rather than the IDE. (It is also possible, though more complicated, to use the IDE. It may also be possible to use GCC or Clang; let me know the results if you try either.)

The first dependency is MPIR, the Windows-friendly port of GMP.

Download YASM (the general use version suffices; don't bother with the version that integrates with Visual Studio) and put yasm.exe somewhere in your path.

Download MPIR and unpack it into e.g. C:\mpir. (If you put it somewhere else, modify subsequent instructions accordingly.)

Open a command window with the C++ compiler environment variables set, and:

cd \mpir\win

If you are building on a 32-bit system it may be necessary to change some occurrences of 'Program Files (x86)' in the above batch files to 'Program Files'.

The other dependency is Boost.

Download Boost and unpack it into e.g. C:\boost. (If you put it somewhere else, modify subsequent instructions accordingly.)

In the command window:

cd \boost
b2 address-model=64 link=static runtime-link=static variant=release

For a 32-bit build, change 64 to 32.

Finally, unpack Ayane into e.g. C:\ayane and:

cd \ayane