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
Cloning of an LK proof has been moved from algorithms.shlk to algorithms.lk








git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1591 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixes issue 244. The equational and definition rules were added to the clone method.







git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1592 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added cloning to the generation of LK proofs from resolution ones


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1593 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Quantifier rules were added to the clone method.





git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1594 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Adding the third possible way of computing grammars.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1595 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Reverting the changes in cli.sh

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1596 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixing typo in cut-intro methods

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1597 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Changes on the veriT parsing.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1598 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
* Integrated miniSAT into cutIntroduction. improveSolution2 now calls miniSAT instead of the bottom-up LK prover to check for tautologies. It can be tested via cutIntro3 in the shell.
* Inserted debug-messages to provide performance information about improveSolution and improveSolution2.
* Deleted utils/ds/lists.scala and merged its one function into utils/dssupport/listSupport.scala

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1599 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixed the bug causing failures in the creation of binary LK rules. The reason was that variable renaming was not always applied. Fixes the farmer's riddle and some others.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1600 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
small change in the last commit

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1601 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Mostly schema code which was waiting some fixes.





git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1602 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Applied the remarks to revision 1602




git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1603 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
some debug info was commented out.




git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1604 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Removed AbsInScope from hol2fol.


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

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


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