Thu, 05 Jul 2007 20:01:26 +0200 |
wenzelm |
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
|
file |
diff |
annotate
|
Thu, 25 May 2006 11:52:33 +0200 |
mengj |
A new "spass" method.
|
file |
diff |
annotate
|
Tue, 07 Mar 2006 03:49:26 +0100 |
mengj |
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
|
file |
diff |
annotate
|
Thu, 23 Feb 2006 12:57:39 +0100 |
mengj |
vampire/eprover methods can now be applied repeatedly until they fail.
|
file |
diff |
annotate
|
Sat, 21 Jan 2006 23:22:40 +0100 |
mengj |
Ensure dereference is delayed.
|
file |
diff |
annotate
|
Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
Mon, 28 Nov 2005 07:13:43 +0100 |
mengj |
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
|
file |
diff |
annotate
|
Fri, 18 Nov 2005 07:06:07 +0100 |
mengj |
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
|
file |
diff |
annotate
|
Fri, 28 Oct 2005 02:28:20 +0200 |
mengj |
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
|
file |
diff |
annotate
|
Wed, 19 Oct 2005 10:25:46 +0200 |
mengj |
*** empty log message ***
|
file |
diff |
annotate
|
Wed, 19 Oct 2005 06:33:24 +0200 |
mengj |
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
|
file |
diff |
annotate
|