OKlibrary  0.2.1.6
ATP.hpp File Reference

Plans regarding installation of automated theorem provers. More...

Go to the source code of this file.


Detailed Description

Plans regarding installation of automated theorem provers.

Todo:
ACL2
Todo:
Prover 9
  • http://www.cs.unm.edu/~mccune/prover9/
  • Installation:
    ExternalSources/Installations/Prover9> tar -xzf $OKPLATFORM/ExternalSources/sources/Prover9/LADR-Dec-2007.tar.gz
    ExternalSources/Installations/Prover9> cd LADR-Dec-2007/
    LADR-Dec-2007> make all
    LADR-Dec-2007> make test1
    LADR-Dec-2007> make test2
    LADR-Dec-2007> make test3
    LADR-Dec-2007> bin/prover9 --version
       
  • DONE Otter http://www.mcs.anl.gov/AR/otter/ ? (it seems that it was replaced by Prover9)
Todo:
Maude
Todo:
First-order theory of the reals
Todo:
Vampire

Definition in file ATP.hpp.