Mon, 04 Aug 2014 16:53:09 +0200 |
blanchet |
deal with E definitions
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 15:02:02 +0200 |
blanchet |
cleaner 'compress' option
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 13:16:18 +0200 |
blanchet |
tuned terminology (cf. 'isar_proofs' option)
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 12:28:42 +0200 |
blanchet |
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
|
file |
diff |
annotate
|
Sat, 02 Aug 2014 00:15:08 +0200 |
blanchet |
better duplicate detection
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 23:58:42 +0200 |
blanchet |
normalize conjectures vs. negated conjectures when comparing terms
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 23:33:43 +0200 |
blanchet |
tweaked 'clone' formula detection
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 23:29:50 +0200 |
blanchet |
fine-tuned Isar reconstruction, esp. boolean simplifications
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 23:29:49 +0200 |
blanchet |
centralized boolean simplification so that e.g. LEO-II benefits from it
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 20:44:29 +0200 |
blanchet |
better handling of variable names
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 20:08:50 +0200 |
blanchet |
nicer generated variable names
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 19:44:18 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 19:36:23 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 19:32:10 +0200 |
blanchet |
more precise handling of LEO-II skolemization
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 16:07:34 +0200 |
blanchet |
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
added appropriate method for skolemization of Z3 steps to the mix
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Whitespace and indentation correction.
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch hilbert_choice_support
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
veriT changes for lifted terms, and ite_elim rules.
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Subproofs for the SMT solver veriT.
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Basic support for the SMT prover veriT.
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 14:03:11 +0200 |
fleury |
Skolemization support for leo-II and Zipperposition.
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 00:50:41 +0200 |
blanchet |
also try 'metis' with 'full_types'
|
file |
diff |
annotate
|
Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
refined filter for ATP steps to avoid 'have True' steps in E proofs
|
file |
diff |
annotate
|
Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
|
file |
diff |
annotate
|
Tue, 24 Jun 2014 08:19:22 +0200 |
blanchet |
supports gradual skolemization (cf. Z3) by threading context through correctly
|
file |
diff |
annotate
|
Tue, 24 Jun 2014 08:19:22 +0200 |
blanchet |
given two one-liners, only show the best of the two
|
file |
diff |
annotate
|
Tue, 24 Jun 2014 08:19:22 +0200 |
blanchet |
don't generate Isar proof skeleton for what amounts to a one-line proof
|
file |
diff |
annotate
|
Thu, 12 Jun 2014 17:10:12 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
Thu, 22 May 2014 05:23:50 +0200 |
blanchet |
properly reconstruct helpers in Z3 proofs
|
file |
diff |
annotate
|
Thu, 22 May 2014 03:29:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 16 May 2014 19:14:00 +0200 |
blanchet |
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
|
file |
diff |
annotate
|
Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
use 'simp add:' syntax in Sledgehammer rather than 'using'
|
file |
diff |
annotate
|
Sun, 04 May 2014 19:01:36 +0200 |
blanchet |
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
|
file |
diff |
annotate
|
Fri, 14 Mar 2014 11:44:11 +0100 |
blanchet |
consolidate consecutive steps that prove the same formula
|
file |
diff |
annotate
|
Fri, 14 Mar 2014 11:15:46 +0100 |
blanchet |
undo rewrite rules (e.g. for 'fun_app') in Isar
|
file |
diff |
annotate
|
Fri, 14 Mar 2014 11:05:45 +0100 |
blanchet |
debugging stuff
|
file |
diff |
annotate
|
Fri, 14 Mar 2014 11:05:44 +0100 |
blanchet |
more simplification of trivial steps
|
file |
diff |
annotate
|
Fri, 14 Mar 2014 11:05:37 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
simplified preplaying information
|
file |
diff |
annotate
|
Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
integrate SMT2 with Sledgehammer
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 10:12:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
file |
diff |
annotate
|
Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
more generous Isar proof compression -- try to remove failing steps
|
file |
diff |
annotate
|
Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
do a second phase of proof compression after minimization
|
file |
diff |
annotate
|
Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 23:59:36 +0100 |
blanchet |
rationalized lists of methods
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 23:49:01 +0100 |
blanchet |
extended method list
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
generate comments in Isar proofs
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
tuned behavior of 'smt' option
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
proper fresh name generation
|
file |
diff |
annotate
|