Wed, 09 Feb 2011 17:18:58 +0100 blanchet added "Z3 as an ATP" support to Sledgehammer locally
Wed, 09 Feb 2011 17:18:57 +0100 blanchet remove Z3 wrapper script, which is no longer necessary now that the SMT module generates SMT-LIB compliant files
Wed, 09 Feb 2011 17:18:57 +0100 blanchet added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip