[isabelle] ATP linkup



The development snapshot of 30 September 2005 has this NEWS item:

* Prover support: pre-release of the Isabelle-ATP linkup, which runs
background jobs to provide advice on the provability of subgoals.

Does this include only support for running background jobs, or also
communication with Vampire, as described in the progress report

http://www.cl.cam.ac.uk/users/jm318/papers/FirstYear_Report.pdf ?

If not, is there a time frame for including such support in Isabelle
development snapshot?

I am asking because I have a data structure consistency verification
system (written in ocaml) that parses formulas in Isabelle subset.  I am
using Isabelle to discharge verification conditions, but I am interested
in trying out Vampire in the cases where Isabelle fails.  But if
Isabelle has a connection to Vampire, then I may be able to avoid it.

Thanks,

  Viktor





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.