Fixing bug on naive CNF transformation.

git-svn-id: http://gapt.googlecode.com/svn/trunk@2148 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Optimizing algorithm for renaming of symbols. The problem surfaced when calling the rename method repeatedly on the same variable. This caused the method to always rename x to x0, x1, x2... until reaching the last index. The new implementation finds already what is the last index and uses this (+1) for the new variable name.

git-svn-id: http://gapt.googlecode.com/svn/trunk@2149 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Reimplementation of Tseitin's transformation without using CNF as a sub-procedure. Modifying maxsat so that it uses the new implementation (return type has changed).

git-svn-id: http://gapt.googlecode.com/svn/trunk@2150 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Removing left-overs.

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

git-svn-id: http://gapt.googlecode.com/svn/trunk@2152 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed some bugs in robinson to ral, bug fixes to ral (one in sub still pending)

git-svn-id: http://gapt.googlecode.com/svn/trunk@2153 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Adding leanCoP-TSTP proofs.

git-svn-id: http://gapt.googlecode.com/svn/trunk@2154 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fix in hol: hol.Equation now matches also Atom(HOLConst(=,Ti->Ti->To), s,t), to have similar behaviour with fol.Equation. The implementation has a handwrritten unapply method, if you know a better solution, please tell me. bug fixes in ral (handles non-idempotent substitutions correctly), robinson to ral

git-svn-id: http://gapt.googlecode.com/svn/trunk@2155 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Modified toDeep.apply to take polarity into account. Added a unit test to verify that toDeep works correctly.


git-svn-id: http://gapt.googlecode.com/svn/trunk@2156 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Added multi expansion sequents and a toDeep function for both trees and sequents to multiExpansionTrees.


git-svn-id: http://gapt.googlecode.com/svn/trunk@2157 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Can now compress ExpansionSequents as well as individual ExpansionTrees.


git-svn-id: http://gapt.googlecode.com/svn/trunk@2158 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Added an algorithm that, given a MultiExpansionSequent, computes the list of valid MultiExpansionSequents below the argument. There is also a small unit test.


git-svn-id: http://gapt.googlecode.com/svn/trunk@2159 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fix for ivy to robinson, robinson paramodulation checks rewriting, more fixes for robinson to ral

git-svn-id: http://gapt.googlecode.com/svn/trunk@2160 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Merge remote-tracking branch 'svn/trunk'