Thu, 30 Jan 2014 20:39:49 +0100 unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
blanchet [Thu, 30 Jan 2014 20:39:49 +0100] rev 55192
unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
Thu, 30 Jan 2014 18:37:08 +0100 killed needless pass
blanchet [Thu, 30 Jan 2014 18:37:08 +0100] rev 55191
killed needless pass
Thu, 30 Jan 2014 16:30:01 +0100 dependency reporting for code generation errors
haftmann [Thu, 30 Jan 2014 16:30:01 +0100] rev 55190
dependency reporting for code generation errors
Thu, 30 Jan 2014 16:30:00 +0100 more abstract dictionary construction
haftmann [Thu, 30 Jan 2014 16:30:00 +0100] rev 55189
more abstract dictionary construction
Thu, 30 Jan 2014 16:09:04 +0100 reduced prominence of "permissive code generation"
haftmann [Thu, 30 Jan 2014 16:09:04 +0100] rev 55188
reduced prominence of "permissive code generation"
Thu, 30 Jan 2014 16:09:03 +0100 split rules for of_bool, similar to if
haftmann [Thu, 30 Jan 2014 16:09:03 +0100] rev 55187
split rules for of_bool, similar to if
Thu, 30 Jan 2014 17:34:42 +0100 don't forget the last inference(s) after conjecture skolemization
blanchet [Thu, 30 Jan 2014 17:34:42 +0100] rev 55186
don't forget the last inference(s) after conjecture skolemization
Thu, 30 Jan 2014 16:40:31 +0100 centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)
blanchet [Thu, 30 Jan 2014 16:40:31 +0100] rev 55185
centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)
Thu, 30 Jan 2014 15:01:40 +0100 keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet [Thu, 30 Jan 2014 15:01:40 +0100] rev 55184
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
Thu, 30 Jan 2014 14:37:53 +0100 renamed Sledgehammer options for symmetry between positive and negative versions
blanchet [Thu, 30 Jan 2014 14:37:53 +0100] rev 55183
renamed Sledgehammer options for symmetry between positive and negative versions
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip