a test variant of the SHLK parser and a test file for the sQMON proof.






git-svn-id: https://gapt.googlecode.com/svn/trunk@1091 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Adding changes for the cut-introduction algorithm. There are still a few bugs, that's why the tests are commented out.

git-svn-id: https://gapt.googlecode.com/svn/trunk@1092 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
object SchemaProofLinkRule was creating a proof-link using the FOFactory.
In the First-order schemata this is not possible any more, so a similar
object that uses the HOLFactory was created. 
In the future I think that the FOFactory even for propositional schema should 
be removed completely?






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