Wed, 24 Aug 2011 11:17:33 +0200 |
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
|
file | diff | annotate |
Tue, 23 Aug 2011 18:42:05 +0200 |
clean up Sledgehammer tactic
|
file | diff | annotate |
Mon, 22 Aug 2011 15:02:45 +0200 |
pass sound option to Sledgehammer tactic
|
file | diff | annotate |
Fri, 10 Jun 2011 12:01:15 +0200 |
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
|
file | diff | annotate |
Mon, 06 Jun 2011 20:56:06 +0200 |
Metis code cleanup
|
file | diff | annotate |
Mon, 06 Jun 2011 20:36:35 +0200 |
more preparations towards hijacking Metis
|
file | diff | annotate |
Tue, 31 May 2011 16:38:36 +0200 |
compile
|
file | diff | annotate |
Mon, 30 May 2011 17:00:38 +0200 |
minimize with Metis if possible
|
file | diff | annotate |
Fri, 27 May 2011 10:30:08 +0200 |
handle non-auto try case of Sledgehammer better
|
file | diff | annotate |
Fri, 27 May 2011 10:30:07 +0200 |
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
|
file | diff | annotate |
Sun, 22 May 2011 14:51:42 +0200 |
improved Waldmeister support -- even run it by default on unit equational goals
|
file | diff | annotate |
Mon, 02 May 2011 22:52:15 +0200 |
tuning
|
file | diff | annotate |
Mon, 02 May 2011 22:52:15 +0200 |
have each ATP filter out dangerous facts for themselves, based on their type system
|
file | diff | annotate |
Sun, 01 May 2011 18:37:25 +0200 |
restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
|
file | diff | annotate |
Sun, 01 May 2011 18:37:25 +0200 |
implement the new ATP type system in Sledgehammer
|
file | diff | annotate |
Thu, 21 Apr 2011 22:18:28 +0200 |
detect some unsound proofs before showing them to the user
|
file | diff | annotate |
Thu, 21 Apr 2011 18:39:22 +0200 |
cleanup: get rid of "may_slice" arguments without changing semantics
|
file | diff | annotate |
Thu, 21 Apr 2011 18:39:22 +0200 |
implemented general slicing for ATPs, especially E 1.2w and above
|
file | diff | annotate |
Sat, 16 Apr 2011 16:15:37 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
Thu, 24 Mar 2011 17:49:27 +0100 |
specify proper defaults for Nitpick and Refute on TPTP + tuning
|
file | diff | annotate |
Wed, 23 Mar 2011 10:06:27 +0100 |
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
|
file | diff | annotate | base |