The SHLK parser for First-order schema has been successfuly used for
parsing the sQMON example.
Take in mind that f^k(x) is represented with the t.r.s. :

g(0,x)   -> x
g(k+1,x) -> f(g(k, x))

The next step is to add a definition rules which deal with the rewriting.
The instead the formula P(f(g(k, x))) we will directly parse P(f(k+1, x)) having
in mind that "f" is a one-place function symbol.









git-svn-id: https://gapt.googlecode.com/svn/trunk@1094 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Implemented functionalities for more than one quantified formula on cut introduction algorithm.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1095 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Cut introduction algorithm now builds a proof with one cut.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1096 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Removing a debug printing.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1097 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
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