Fixed computation of the decompositions' sizes.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1098 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Formula highlighting is added to prooftool.

Simply move cursor to over formula and it will become blue (it is the case in every object, proofs, trees, lists)

git-svn-id: https://gapt.googlecode.com/svn/trunk@1099 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed sorting bug, polished output

git-svn-id: https://gapt.googlecode.com/svn/trunk@1100 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Chain of terms f(f ... f(t)) are displayed as f^n(t).

Feature is not well tested (tried only for cut-introduction example), so if you find any bug please tell me.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1101 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixed the contractions on the cut-introduction algorithm plus some polishing.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1102 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added new example proof sequence for testing cut-introduction (2 quantified formulas with 2 quantifiers each in the end-sequent)

git-svn-id: https://gapt.googlecode.com/svn/trunk@1103 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added vscaladoc plugin. you can call it using mvn site or mvn scala:doc

git-svn-id: https://gapt.googlecode.com/svn/trunk@1104 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
just noticed that vscaladoc doesnt support scala 2.9, reverting to scaladoc (you can still call it using mvn site, etc.)

git-svn-id: https://gapt.googlecode.com/svn/trunk@1105 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
more example proof sequences for testing cut-introduction algorithm

git-svn-id: https://gapt.googlecode.com/svn/trunk@1106 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixed term set computation bug.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1107 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Continuing from another computer.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1108 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixing issue 193. And now the square diagonal example works :)

git-svn-id: https://gapt.googlecode.com/svn/trunk@1109 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Had to change the method for DB indices on schema.scala also to make it override the right method (an argument was added...). It doesn't look like this method is beeing used anywhere, but those that use that implementation should check, please.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1110 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
spelling, indentation

git-svn-id: https://gapt.googlecode.com/svn/trunk@1111 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
A schematic version for the proof with end sequent:

Forall x (Imp P(x) P(f(x))) |- Forall x (Imp P(x) P(f^(2^k)(x)))

which Alex asked me to type in the SHLK before he went on vacation.
P.S. This is also an example from the iCERES which Stefan coded.






git-svn-id: https://gapt.googlecode.com/svn/trunk@1112 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Some usability enhancements, in particular introduced some structure to
the CLI-help screen - constructive critisims and suggestions are welcome


git-svn-id: https://gapt.googlecode.com/svn/trunk@1113 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Integrated SLK parsing into the CLI.
Finished the SLK example "sEXP.lks".



git-svn-id: https://gapt.googlecode.com/svn/trunk@1114 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Some conflicts are resolved





git-svn-id: https://gapt.googlecode.com/svn/trunk@1115 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fix the previous commitment.





git-svn-id: https://gapt.googlecode.com/svn/trunk@1116 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixed after the small changes in schema.scala.
P.S. Stefan, this is related to the your remark from yesterday.





git-svn-id: https://gapt.googlecode.com/svn/trunk@1117 85d21ef8-add0-11de-ae77-5bfb9c5a3f34