I am pretty new to ATP, but I'm really enjoying playing around with prover9. I have found a nice set of axioms for basic information-theoretic proofs here, I was wondering if there are some collections of axioms for other purposes too, e.g. probability theory.

I found a gigantic set of axioms for TPTP programs here, but prover9 is a LADR program...

  • $\begingroup$ Don't forget to also use mace4, I found it even more useful than prover9. LADR just means "Library for Automated Deduction Research", and has little to do with the file format. The-E-theorem-prover can directly use TPTP programs. But I found it quite easy to convert between the different input formats, so I wouldn't worry too much about the file format. Here I describe some of my own experiments with prover9 & co. $\endgroup$ – Thomas Klimpel May 19 '15 at 18:47
  • $\begingroup$ If I understand correctly, you are saying that it is sufficient to translate files from the TPTP format to a format that prover9 would understand? $\endgroup$ – Ziofil May 20 '15 at 15:21
  • 1
    $\begingroup$ I think the TPTP library also contains a utility called TPTP2X, which can convert to the input format of many different ATP systems. As you can see from the linked page, prover9 is also among the supported TPTP2X Output Formats. $\endgroup$ – Thomas Klimpel May 20 '15 at 15:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.