pushed to latest library versions, added an alternative clause set generation algorithm which handles bigger structs better(cvetan's algorithm was a normlization procedure on structs, which can create deep nestings which overflow the call stack)

git-svn-id: https://gapt.googlecode.com/svn/trunk@2344 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed a compiler warning in fol matching (an Option[X] was compared to [X]). Corrected the code, but i'm not 100% sure if this what should have been compared in the first place.

git-svn-id: https://gapt.googlecode.com/svn/trunk@2345 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Implementing a more general grammar

The Grammar class goes from supporting only
grammars of the type U o S to supporting the more
genral grammar format U o S1 o ... o Sn, which is
needed for the introduction of many cuts.

Thanks to Christoph Spoerk for this change.

git-svn-id: https://gapt.googlecode.com/svn/trunk@2346 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added glue code (partial reversing of hol2fol) to ntape tests, bugfixes in robinson2ral and ceres omega.

git-svn-id: https://gapt.googlecode.com/svn/trunk@2347 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed cutIntro integration tests
added scala doc to Grammar class for the constructor

git-svn-id: https://gapt.googlecode.com/svn/trunk@2348 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
ntape proof acnf and et computed in ntape test

git-svn-id: https://gapt.googlecode.com/svn/trunk@2349 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
some more bugfixes to ceres omega

git-svn-id: https://gapt.googlecode.com/svn/trunk@2350 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
implemented (hopefully correct) skolem symbol merging. et calculation is working now.

git-svn-id: https://gapt.googlecode.com/svn/trunk@2351 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
sorry for breaking the build, this should fix it

git-svn-id: https://gapt.googlecode.com/svn/trunk@2352 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
I renamed the "ancestors" member of FormulaOccurrence to "parents" to reflect that it only contains immediate predecessors. I also added a function "ancestors" that returns the actual ancestors.


git-svn-id: https://gapt.googlecode.com/svn/trunk@2353 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixing path of prover9 minitests

git-svn-id: https://gapt.googlecode.com/svn/trunk@2354 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Prover9 import should now work again. The biggest issue was that the equality rules didn't cover the case of trivial rules, i.e. the equation is of the form s=s and the auxiliary and main formulas coincide.


git-svn-id: https://gapt.googlecode.com/svn/trunk@2355 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Adding a verbose argument to extraction of Expansion Trees

git-svn-id: https://gapt.googlecode.com/svn/trunk@2356 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Adding gitignore file.
Removing println from StandartClauseSet.
Removing logging

The logging mechanism, although useful, is being
in my opinion overly used in gapt. We shouldn't
use logging for debugging, and we shouldn't leave
debugging lines in the main repository code. Also,
making a class extend yet another interface is
really overloading its responsabilites and the
code is often harder to read with all the
debugging lines around. Another reason I can think
of for removing the logging from all these files
is the fact that we either need to keep a very
long (and constantly needing updates) log4j file
or we live with its warning messages.
For running the cut-introduction experiments, the
only logging that is left is the one in the test
script itself, and no other if I can help it.