The missing parts of the usual CERES method 
were connected and integrated in CLI. It should be tested now.
So far it was tested on an instance of a proof schema. This
can be executed in CLI using the following commands:


1. parse.slk("/home/cvetan/resources/sEXP.lks")

2. val p = unfoldProof("\\psi",2)

3. val struct = extractStruct(p)

4. val ccs = structToClausesList(struct)

5. val robinsonResProof = prover9(ccs).get

6. val groundSubst = prover9.getGroundSubstitution(robinsonResProof)

7. val resProofToFOLLKProof = Robinson2LK(robinsonResProof)

8. val FOLLKProofToHOLLKProof = Robinson2LK.toHOL(resProofToFOLLKProof)

9. val setOfProjections = computeProjections(p)

10. val groundProjections = computeGroundProjections(setOfProjections, groundSubst)

11. val acnf = buildACNF(FOLLKProofToHOLLKProof, groundProjections, p.root.toFSequent)

12. prooftool(acnf)










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