fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57705
Subproofs for the SMT solver veriT.
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57704
Basic support for the SMT prover veriT.
fleury [Wed, 30 Jul 2014 14:03:11 +0200] rev 57703
removing the '= True' generated by Leo-II.
fleury [Wed, 30 Jul 2014 14:03:11 +0200] rev 57702
Skolemization support for leo-II and Zipperposition.
desharna [Wed, 30 Jul 2014 10:50:30 +0200] rev 57701
document property 'set_induct'
desharna [Wed, 30 Jul 2014 10:50:28 +0200] rev 57700
generate 'set_induct' theorem for codatatypes
blanchet [Wed, 30 Jul 2014 00:50:41 +0200] rev 57699
also try 'metis' with 'full_types'
blanchet [Tue, 29 Jul 2014 23:39:35 +0200] rev 57698
header tuning
blanchet [Mon, 28 Jul 2014 10:57:33 +0200] rev 57697
correctly translate THF functions from terms to types
blanchet [Sun, 27 Jul 2014 21:11:35 +0200] rev 57696
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly