fixed transformation from ivy resolution to robinson resolution. shared nodes were duplicated which is a problem in the case of GRA014+1: the prover9 refutation has 210 inferences, the ivy refutation has 479 and the ground refutation has 18042747

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1277 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Reverting changes that did not fix issue 206.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1278 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
loadProver9Proof in the cli now parses prover9 output, the new prover9(filename : String) refutes a file given in ladr format (have to find a better name for this)

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1279 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
1) created MultiExpansionTree which is the same as ExpansionTree but allow for vectors of selected/expanded terms
2) created an algorithm which compresses a tree into a multiTree for sequential quantifiers of the same type
3) added the relevant method to cli



git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1280 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
The set of all proof projections is extracted from the normalized (grounded) projection term.

 




git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1281 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Instantiation of ProjectionTerm schema is integrated in prooftool.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1282 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
A typo.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1283 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
In my previous comment, in the ProjectionTerm.scala there was a "TODO:" gap in the 
UnfoldProjectionTerm object. Now it is implemented.









git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1284 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed naming scheme for ivy parser - GEO037-2.ivy is still not parsable because it contains a paramodulation step (halfway implemented but still buggy and without translation to robinson resolution)

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1285 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
The bug in the unfolding of normalized projection terms was fixed. 

Wieder alles in Ordnung. :)










git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1286 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
two examples were modified.





git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1287 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Meanwhile another bug was found and fixed. The projection extraction, instantiation
and unfolding can be seen also in ProofTool for arbitrary instance.







git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1288 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
ExpansionTrees improved: single instance is drawn inside <> as well and left mouse clicking is added to open/expand a quantifier.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1289 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
parsing of paramod and flip works now, translation to robinson proofs is still buggy

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1290 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
A new test for the schema projection term has been added.







git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1291 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixes issue 206.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1292 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
typo

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1293 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
A small bug in struct extraction is fixed.




git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1294 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Handling of nested quantifiers in ExpansionTree is corrected in ProofTool. One such test is added in the Test menu.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1295 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
During the last project meeting Alex proposed to replace the cl^{(proof, \Omega)} symbols
in the displaying with symbols which do not contain the useless for the user information 
such as proof name and omega-configuration. Now they are replaced with unique 
HOLConsts of type \omega -> o








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