fixed a bug in the prover9 term parser: multiple literals per inference step were not allowed. also there is now Prover9TermParserLadrStyle which implements LADR style variable naming and autodetection code while loading files. the ET paper example works now, please use 'prooftool(loadProver9LKProof( provers/prover9/src/test/resources/cade13example.out))' to load it

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1380 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
changed the PCNF algorithm not to compute partitions but to take the whole context. The duplicated formulas are later contracted



git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1381 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Hardcoded example for cade paper.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1383 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
- Added a top level function (getDecompositions) that returns a list with all the
  decompositions (sorted by size).
- Now the function "improveCanonicalSolution" in CLI returns a list of the
  possible simplifications sorted by size.
- The main code for cut introduction now uses the improved solution.
- Should we change "decomposition" to "grammar" (at least at the top level so
  not to confuse the user)?
- Tried to fix the bug pointed out by Stefan in r1361. Now ForgetfulResolution
  finds the solution he proposed (¬P(x)∨P(s^3(x))) but it states that it is not
  a valid solution. Is it? I haven't checked.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1384 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Hardcoded example for cade paper: a typo.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1385 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Hardcoded example for cade paper: a typo.

P.S. Sorry for many commits, but I'm compiling over the network. 


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1386 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Just a version change.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1387 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
loadProver9LKProof now detects if the input formula is not skolemized and instead uses the clauses to create the endsequent.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1391 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
removed debug message from RobinsonToLK

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1392 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Merge branch 'master' of ssh://github.com/newca12/gapt into m2e