now extracting endsequent directly from prover9's outfile instead of passing it through prooftrans xml

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1404 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed a problem with variable renaming. The problem with different constants still persists though


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1405 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed a small problem with regard to the previous commit


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1406 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed a stupid bug which prevent the new version of end-sequent extraction to be used

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1407 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
rollbacked the projections up to variable renamings and added a map for computed proofs in order not to compute more than once the same proof.
the variable renaming should be probably handled in prover9. I will add a normalization process there.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1408 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1409 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
- removed the computeAux in quantifiers which was incorrect. This fixes the bug.
- since we aim at expansion trees and not the correct LK proofs, I also remove all weakening introductions in the computation of the LK proof. The weakenings
made the proof too big for our weak data structures to handle. Now I think more examples will go through although the computation of the LK proof is not precise now.
I can also make it precise by adding possible weakenings to the end-sequent but since this information is completely useless to the users of the expansion trees
I decided not to.
- with regard yo variable renaming. Martin already solved the problem. When the end-sequent is not skolemized, then he computes it from the resolution proof.
Since the original end-sequent is again, not important for the computation of expansion trees, I added another boolean field for computing the end-sequent
in such a way anyway, you can call it for example:
loadProver9LKProof("../../testing/prover9-TSTP/ALG/ALG012-1/Prover9---1109a.UNS-Ref.s.out",true,true)
if this solution is ok with everybody, we can make it the default behavior
This solves the problem with variable renaming



git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1410 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
setting the Martin's read endsequent from refutation as the default behaviour



git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1411 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Small change in prooftool to show dbindex of bound variables.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1412 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
- removed the default option to read endsequent from resproof
- returned variable renaming and apply contractions also on the clause in the projections.
- still has a problem with proofs where the theorem is in CNF already as then none of the variables instantiated is bound. can it be that we need to universally quantifies over this variables?


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1413 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added Ex/AllVarInScope(x,f) where the variable x remains a bound variable. Mikheil, please you these extractors when you build the latex string


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1414 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Small change in prooftool to show dbindex of bound variables.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1415 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
closed the formulas in end-sequent extraction. A[x] :- B[y] will become all x A :- exists x B, hope this is now correct (from a logical point it should be ok since exists x (Ax | Bx) implies (exists x Ax) | (exists x Bx) but i'm not sure we actually want this

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1416 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
- Fixes issue 227.
- Changed the help text from "ceresHelp" to "help".
- Fixed the interface of some methods from cut-introduction.
- cutIntro now tries all the smallest grammars and chooses the one that
  generates the smallest proof.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1418 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added release detection code to cli.sh

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1420 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
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
fixes issue 230 : will take the first proof if more than one proof object is present. ; new_symbol elimination started but not finished(found new bug in ivy parser)

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1424 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
ivy parser accepts now demodulation, does not convert to paramod though

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