prooftool can now display a struct passed from the cli. made parts of struct to css conversion tailrecursive to handle bigger clause sets (clause set extraction fails with stack overflow), added size calculation to StructCreators, added SimplifyStruct which removes trivial tautologies and (some) empty children.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1777 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
bug fix in struct optimization code

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1778 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Added isValid method to Prover9 that runs Prover9 but does not parse the proof in order to save time.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1780 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
needed to move rewriting to lkalgorithms, added tautology completion to atomic axioms for proofs, added tactics for llk macro rules

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1781 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
prepartations for next test run of cut-introduction:
* adding method to compute logical complexity of a HOLFormula
* adding method to transform an expansion proof into an expansion proof modulo equality to testCutIntro


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