2006-05-25 mengj 2006-05-25 A new "spass" method.
2006-03-07 mengj 2006-03-07 When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
2006-02-23 mengj 2006-02-23 vampire/eprover methods can now be applied repeatedly until they fail.
2006-01-21 mengj 2006-01-21 Ensure dereference is delayed.
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-11-28 mengj 2005-11-28 Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. Still have old verions of "vampireH","vampireF", "eproverH", "eproverF", which can be called to handle HOL or FOL problems.
2005-11-18 mengj 2005-11-18 -- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
2005-10-28 mengj 2005-10-28 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.
2005-10-19 mengj 2005-10-19 *** empty log message ***
2005-10-19 mengj 2005-10-19 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").