The parser for resolution schemata is already in progress. 







git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1301 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
The rewriting systems for the s-terms and resolution schemata are now global objects.
Before use them in a test the clean() method should be called.






git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1302 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
a small bug is fixed






git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1303 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
The substitution of the second-order variables in a ground resolution term works.
The parser can not parse such a substitution yet, but soon it will be implemented.





git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1304 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
a small bug is fixed.





git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1305 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
First steps to integrate resolution schema parser in ProofTool.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1306 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
The parsing and unfolding of a resolution schemata is ready. Only the parsing
of the second-order substitution is not ready, but when it is hard-coded
everything works fine. A resolution refutation which verifies the
correctness of the resolution schemata (see the .rs file) is also produced.


IMPORTANT: For the resolution refutation which uses a cut-rule I had to change in calculus/lk 
the usual equiality "==" between HOLFormulas with the syntaxEquals. Otherwise the 
CutRule(...) can not be applied. This happens for first time to me! 
But indeed it is correct in this case. So, syntaxEquality should be 
used everywhere in my oppinion.







git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1307 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
The parsing of a second-order substitution is integrated. A resolution refutation
for a given instance could be produced.





git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1308 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Next step to integrate resolution schema parser in ProofTool.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1309 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added efficient size method for large agraphs; added cli command prover9.refuteTPTP to call prover9 with a tptp file; started renaming of symbols in resolution proofs;

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1310 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixes issue 221: if a proof contains the constant nil this will be interpreted as the empty list by a lisp parser. empty lists as part of terms are now interpreted as the constant nil (as we cannot resolve the ambiguity all of the time, we opt to parse the term if we are not sure)

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1311 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Nested expansion tree example is changed.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1312 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Some unicodes were removed, because the Mac does not accept them.





git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1313 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fix issue 210


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1314 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed a problem in robinson2LK where the aggregated substitution was not considered. Bug 212 still holds though and the initiative is returned (for now) to Martin


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1315 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fix m2e integration
Yet another fix for m2e integration
Get rid of maven plugin management
ugly fake commit to merge master