Fixes issue 226.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1421 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Changed the interface of more methods for the cut-introduction algorithm. Now
the commands to generate a proof step-by-step are:

// Creates the proof
scala> val p = LinearEqExampleProof(4)

// Extracts the terms
scala> val ts = extractTerms(p)
The term set contains 9 terms.

// Compute the grammars
scala> val grms = computeGrammars(ts)
30 grammars found.

// See the grammars to choose from
scala> seeNFirstGrammars(grms, 5)
0. { tuple1(a), tuple3(f(α), α, a), tuple2(α),  } o { f(f(f(a))), f(f(a)), f(a), a,  }(size = 7)
1. { tuple1(a), tuple2(f(f(α))), tuple3(f(α), α, a), tuple2(α), tuple3(f(f(f(α))), f(f(α)), a),  } o { f(a), a,  }(size = 7)
2. { tuple1(a), tuple2(f(α)), tuple3(f(f(α)), f(α), a), tuple3(f(α), α, a), tuple2(α),  } o { f(f(a)), a,  }(size = 7)
3. { tuple1(a), tuple3(f(f(f(f(a)))), f(f(f(a))), a), tuple3(f(a), a, a), tuple2(f(f(α))), tuple3(f(f(α)), f(α), a), tuple2(α),  } o { f(a), a,  }(size = 8)
4. { tuple1(a), tuple3(f(f(f(f(a)))), f(f(f(a))), a), tuple3(f(f(f(a))), f(f(a)), a), tuple2(f(f(α))), tuple3(f(α), α, a), tuple2(α),  } o { f(a), a,  }(size = 8)

// Chooses a grammar
scala> val g = grms(0)

// Generates the extended Herbrand Sequent
scala> val ehs = generateExtendedHerbrandSequent(p.root, g)

// Minimizes the solution
scala> minimizeSolution(ehs)
Previous solution: ∀x.(=(f(x), x)∧(=(f(x), x)⊃(=(x, a)⊃=(f(x), a))))
Improved solution: ∀x.(=(f(x), a)∨¬=(x, a))

// Builds the final proof
scala> val fp = buildProofWithCut(ehs)



git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1422 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Updating the help text from cli

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