Started work on prooftool: scrolling to subproofs (in particular, give user
commands to "jump to end-sequent" and "cycle through cuts").
Initial implementation still not working correctly.
Slight refactoring of ReductiveCutElim - the aim is to be able to do a single step of cutelim in prooftool,
which automatically loads the new proof (after that single step), and scrolls to the subproof which was reduced.



git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1444 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Refactored cut-elimination a bit. It is now more flexible and supports
strategies (see the comments in the code).

You can do the following in the CLI to see how to do Gentzen-style
cut-elimination and one-step uppermost cut-reduction by giving appropriate
predicates that control termination and choice of cut-to-be-reduced.



import at.logic.transformations.ReductiveCutElim
import at.logic.calculi.lk.propositionalRules._

val proof = cutIntro(LinearExampleProof(4))

def isCutFree(p: LKProof) = ReductiveCutElim.isCutFree(p)
def isUppermost(p: LKProof) = p match { case CutRule(p1,p2,_,_,_) => isCutFree(p1) && isCutFree(p2) }

// Gentzen-style
ReductiveCutElim(proof, false, {x => false}, { (_, cut) => isUppermost(cut) })

// single-step uppermost
ReductiveCutElim(proof, false, {x => true}, { (_, cut) => isUppermost(cut) } )



Other strategies can be implemented quite simply. Modulo some easy-to-implement functions,
also the following strategies can be used:

// Leftmost-uppermost (need to implement isLeftmostIn)
ReductiveCutElim(proof, false, {x => false}, { (proof, cut) => isUppermost(cut) && isLeftmostIn(proof, cut) })

// only quantified cuts, uppermost (need to implement isUppermostQuantified)
def isQuantifiedCut(p: LKProof) = p match { case CutRule(_,_,_,a,_) => containsQuantifiers(a.formula) }
ReductiveCutElim(proof, false, {x => false}, { (_, cut) => isQuantifiedCut(cut) && isUppermostQuantified(cut) } )

// upto atomic cuts, uppermost (need to implement isUppermostNonAtomic)
def isNonAtomicCut(p: LKProof) = p match { case CutRule(_,_,_,a,_) => a match { case Atom(_,_) => false
                                                                                case _ => true 
                                                                              }
                                         }
ReductiveCutElim(proof, false, {x => false}, { (_, cut) => isNonAtomicCut(cut) && isUppermostNonAtomic(cut) } )



// Tait-style (need to implement weight functions)
ReductiveCutElim(proof, false, {x => false}, { (proof, cut) =>  
                                                 weight(cut) == weight(proof) && isUppermostWithWeight(cut) } )


--------------------------------------------------------------------------------------------------

Added an integration test to MiscTest that introduces a cut for the LinearExampleProof,
and then eliminates it using reductive cut-elimination :-)

--------------------------------------------------------------------------------------------------

I incorporated Mikheil's suggestion, and fixed a bug. Now cycling through cuts in prooftool seems
to work well. Auto-scrolling to the reduced cut after cut-elimination still does not work as intended.





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