added minisat to readme

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1568 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
* Fixed the stack overflow error during cut introduction in Grammar.scala (cutIntro still causes the stack to overflow, but in a different place).
* Put the definition of LK into user_manual.tex

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1570 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
* Added a new, more efficient version of cutIntro which does not perform redundant resolutions in ExtendedHerbrandSequent.improveSolution. For the time being, the new version is called cutIntro2 and the old one has been left as is. Based on a sample of example proofs, cutIntro2's running time is about 20-30% faster than that of cutIntro.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1571 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
moved equational theory parts into unficiation, moved tptp fof export to parsing, export still disabled

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1572 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Putting 'checking_lambda_expression' on the right place and deleting 'freevars_boundvars_constants_of'.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1573 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added failing parse example for issue 242

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

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1575 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
replacing some println's by correct debugging output

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1577 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
reduced cli stacksize to 1M - please test if everything still works.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1578 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added infix term symbols +,-,/,* to the prover9 parser

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1579 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
- Implemented a getTerm method in Substitution.
- Implemented a getMatrix method in fol.scala
- Implemented methods to transform quantifier-free and prenex formulas into
  expansion trees.
- Advancing in veriT parsing.
- Organizing GAPScalaInteractiveShell and creating method to parse veriT proofs.
- Added an import to CLIMain so that testCutIntro could use FlatTermSet
- Modifying testCutIntro to run again


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1580 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
restructured and improved user manual,
some usability improvements


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1582 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Adding more tests for cut-introduction

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1583 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Adapting the veriT parser so that it returns an expansion tree.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1584 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added equational rules to acnf computation, added substitution of free variables in lk proofs (needs more testing for correct treatment of eigenvariable conditions etc), added equational atoms to xml export(we still cannot parse this :( ), started writing a direct grounding of resolution proofs (which should lead to a very simple Robinson2LK transformation)

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1585 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Extended cutIntro2 with a new way to find grammars. cutIntro is unchanged. cutIntro2 is EXPERIMENTAL, as it seems to prune grammars too aggressively, which results in slightly different cut formulas\!

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1586 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fix for last revision: lists.scala wasn't added to source control.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1587 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
removed require(checkFormulaOccurrences) from creation of LK inferences

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

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1589 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
- added interface for passing the projections to the resolution to lk transformation. Note that since the LK proof must be a tree
the projections must be cloned somehow so right now the implementation will not work if a projection is used more than once.
- creating contractions after the application of each binary rule. This is also buggy as I dont check if the contracted formula is required in the resolution proof.
The algorithm will throw an exception anyway if this is the case.



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