Fri, 01 Aug 2014 20:15:41 +0200 | blanchet | try to get rid of skolems first | changeset | files |
Fri, 01 Aug 2014 20:08:50 +0200 | blanchet | nicer generated variable names | changeset | files |
Fri, 01 Aug 2014 19:44:18 +0200 | blanchet | tuning | changeset | files |
Fri, 01 Aug 2014 19:36:23 +0200 | blanchet | tuning | changeset | files |
Fri, 01 Aug 2014 19:32:46 +0200 | blanchet | no need to 'obtain' variables not in formula | changeset | files |
Fri, 01 Aug 2014 19:32:10 +0200 | blanchet | more precise handling of LEO-II skolemization | changeset | files |
Fri, 01 Aug 2014 16:07:34 +0200 | blanchet | beware of 'skolem' rules that do not skolemize (e.g. LEO-II) | changeset | files |