sci-mathematics/otter is now depreciated, and the prover9 project has picked up where it left off. This is an automated theorem prover for first order predicate logic. It also has an optional gtk gui. prover9 seems to be under active development, and it is of stable production quality. Otter is as a matter of fact one of the only fully automated theorem provers of this type in the portage tree. Several key related provers are also missing such as 'e', Isabelle, and acl2. Another prover which deserves a serious look is zenon (http://focal.inria.fr/zenon/). I think prover9 would be a good starting point however. Homepage: http://www.cs.unm.edu/~mccune/mace4/ Source for mace & prover9 suite of command-line applications "LADR": http://www.cs.unm.edu/~mccune/mace4/download/ GUI based on wxpython & prover9 binaries: http://www.cs.unm.edu/~mccune/mace4/gui/v05.html Reproducible: Always Steps to Reproduce: 1. eix prover9 2. Observe the lack of output. 3. Facepalm. Actual Results: Sore forehead resulting from the rapid application of palm to face, as illustrated by these fine examples: http://www.facepalm.org/ Expected Results: Spiffy formal proofs of great truths about the universe. Seems to run perfectly with a manual compile. The best way to go about this is to compile the LADR sources, then download and extract the python gui, delete the included binaries from the GUI bin folder, and replace with the locally compiled programs. The only dependency that I didn't already have was the wxpython package - wxWidgets libs for python. I'm currently working my way through the ebuild documentation, but have yet to create a clean, working ebuild from scratch. I'll attach my progress if nobody else can do this quickly/easily.
Different university url. Same mace4 as in bug 49205 ?
(In reply to comment #1) > Different university url. Same mace4 as in bug 49205 ? > Yeah that looks like the same mace. (mace4) I think mace is intended to be bundled with prover9. Both are integrated into the gui so you can run them at the same time from that.
O.k., then let's keep it in this bug. Feel free to attach better/updated ebuilds there. *** This bug has been marked as a duplicate of bug 49205 ***
