Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fixed detection of Skolem constants in type construction detection code
Mon, 06 Jun 2011 20:36:35 +0200 blanchet make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning
Mon, 06 Jun 2011 20:36:35 +0200 blanchet also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
Mon, 06 Jun 2011 20:36:35 +0200 blanchet reveal Skolems in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
Mon, 06 Jun 2011 20:36:35 +0200 blanchet slacker version of "fastype_of", in case a function has dummy type
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't stumble on Skolem names
Mon, 06 Jun 2011 20:36:35 +0200 blanchet conceal old Skolems in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs
Mon, 06 Jun 2011 20:36:35 +0200 blanchet use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
Mon, 06 Jun 2011 20:36:35 +0200 blanchet properly unmangle names in path finder
Mon, 06 Jun 2011 20:36:35 +0200 blanchet only uncombine combinators in textual Isar proofs, not in Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet properly locate helpers whose constants have several entries in the helper table
Mon, 06 Jun 2011 20:36:35 +0200 blanchet skip "hBOOL" in new Metis path finder
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't pass "~ " to new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning
Mon, 06 Jun 2011 20:36:35 +0200 blanchet gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings
Mon, 06 Jun 2011 20:36:35 +0200 blanchet temporarily document "metisX"
Mon, 06 Jun 2011 20:36:34 +0200 blanchet use "metisX" as fallback, since it's much faster than "metisFT"
Mon, 06 Jun 2011 20:36:34 +0200 blanchet temporarily added "MetisX" as reconstructor and minimizer
Mon, 06 Jun 2011 20:36:34 +0200 blanchet ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
Mon, 06 Jun 2011 20:36:34 +0200 blanchet show what failed to play
Mon, 06 Jun 2011 20:36:34 +0200 blanchet refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
Mon, 06 Jun 2011 20:36:34 +0200 blanchet tuning
Mon, 06 Jun 2011 20:36:34 +0200 blanchet killed odd connectives
Mon, 06 Jun 2011 20:36:34 +0200 blanchet added Metis examples to test the new type encodings
Mon, 06 Jun 2011 20:36:34 +0200 blanchet tuned CASC method
Mon, 06 Jun 2011 20:36:34 +0200 blanchet clean up unnecessary machinery -- helpers work also with monomorphic type encodings
Mon, 06 Jun 2011 20:36:34 +0200 blanchet added support for helpers in new Metis, so far only for polymorphic type encodings
Mon, 06 Jun 2011 16:29:38 +0200 kleing imported rest of new IMP
Mon, 06 Jun 2011 16:29:13 +0200 kleing atLeastAtMostSuc_conv on int
Mon, 06 Jun 2011 14:11:54 +0200 kleing fixed typo
Sun, 05 Jun 2011 15:00:52 +0200 boehmes updated SMT certificates
Sun, 05 Jun 2011 15:00:17 +0200 boehmes made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
Fri, 03 Jun 2011 19:37:26 +0200 bulwahn changing the mira setting again for the mutabelle configuration
Fri, 03 Jun 2011 07:25:44 +0200 bulwahn adding more settings to mira's mutabelle configuration
Thu, 02 Jun 2011 15:17:23 +0200 nipkow merged
Thu, 02 Jun 2011 10:10:23 +0200 nipkow Added typed IMP
Thu, 02 Jun 2011 10:13:46 +0200 bulwahn adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
Thu, 02 Jun 2011 09:51:40 +0200 bulwahn adding invocation of exhaustive testing without using finite types to mutabelle
Thu, 02 Jun 2011 09:51:40 +0200 bulwahn moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle
Thu, 02 Jun 2011 08:55:08 +0200 bulwahn splitting Dlist theory in Dlist and Dlist_Cset
Wed, 01 Jun 2011 23:08:04 +0200 nipkow merged
Wed, 01 Jun 2011 22:47:26 +0200 nipkow Made comments text
Wed, 01 Jun 2011 22:42:37 +0200 nipkow Fixed denotational semantics
Wed, 01 Jun 2011 21:50:49 +0200 nipkow Removed old IMP files
Wed, 01 Jun 2011 21:35:34 +0200 nipkow Replacing old IMP with new Semantics material
Wed, 01 Jun 2011 15:53:47 +0200 nipkow tuned lemmas
Wed, 01 Jun 2011 19:50:59 +0200 blanchet fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2
Wed, 01 Jun 2011 13:50:37 +0200 bulwahn setting up code generation for extended reals
Wed, 01 Jun 2011 11:51:25 +0200 nipkow new lemmas
Wed, 01 Jun 2011 10:29:43 +0200 blanchet handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
Wed, 01 Jun 2011 10:29:43 +0200 blanchet more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
Wed, 01 Jun 2011 10:29:43 +0200 blanchet make sure no warnings are given for polymorphic facts where we use a monomorphic instance
Wed, 01 Jun 2011 10:29:43 +0200 blanchet fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume"
Wed, 01 Jun 2011 10:29:43 +0200 blanchet ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
Wed, 01 Jun 2011 10:29:43 +0200 blanchet fixed interaction between type tags and hAPP in reconstruction code
Wed, 01 Jun 2011 10:29:43 +0200 blanchet implemented missing hAPP and ti cases of new path finder
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip