Re: [isabelle] Isabelle-Oracle Interface



Tuvshintur,

On Thursday 14 December 2006 10:18, Tuvshintur Tserendorj wrote:
> i heard that Isabelle has a oracle interface for communicating with
> extern programs. However, I could'nt find any examples in the internet.
>
> Could anybody tell me how i can use the oracle interface of isabelle?
> Where can i find any docus about that?

see Chapter 6.10 of the Isabelle Reference Manual [1] for some documentation.  
An "oracle" is essentially just an ML function which returns theorems.  Of 
course you are free to call external programs (or do whatever else you want) 
in this ML function.

There are many examples of oracle implementations in the Isabelle 
distribution, see e.g. HOL/ex/SVC_Oracle.thy and related files.

Best,
Tjark

[1] http://isabelle.in.tum.de/dist/Isabelle/doc/ref.pdf





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