search

asr / apia

Haskell program for proving first-order theorems written in Agda using automatic theorem provers for first-order logic
MIT License
6 stars 0 forks source link

Feature/onlineatps #59

Closed jonaprieto closed 8 years ago

jonaprieto commented 8 years ago

This gives support to use onlineatps.

jonaprieto commented 8 years ago

I don't how to fix this error in travis. It's not clear. Can you help me?

asr commented 8 years ago

I don't how to fix this error in travis. It's not clear. Can you help me?

Could you reproduce locally the error? That is, which is the output of make non_conjectures?

asr commented 8 years ago

I don't understand why your PR includes some commits from the master branch. Create a "clean" PR please.

asr commented 8 years ago

I don't understand why your PR includes some commits from the master branch. Create a "clean" PR please.

Forget what I said.

asr commented 8 years ago

Using the Test.agda file in the README.md, I got the following results:

$ apia --atp=e Test.agda
Proving the conjecture in /tmp/Test/9-8744-comm.fof
E 1.9 Sourenee proved the conjecture
apia --atp=online-e Test.agda
Proving the conjecture in /tmp/Test/9-8744-comm.fof
E---2.0 *did not* prove the conjecture
apia: the ATP(s) did not prove the conjecture in /tmp/Test/9-8744-comm.fof

That is, I couldn't prove the conjecture using the --atp=online-e option.

asr commented 8 years ago

Good job! Please fix the small details I pointed-out and I'll merge the PR.

asr commented 8 years ago

The PR has conflicts with master, so I cannot merge it. Please push a commit fixing the conflicts.

jonaprieto commented 8 years ago

I will open a new PR. It is not easy to solve the conflicts.