Email Gateway (Aug 18 2022 at 10:00): Email Gateway (Aug 18 2022 at 10:00):From: Tuvshintur Tserendorj <uesn@cs.tu-berlin.de>
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?
Thanks.
Cheers,
Tuvshintur
Email Gateway (Aug 18 2022 at 10:00):From: Tjark Weber <tjark.weber@gmx.de>
Tuvshintur,
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
Email Gateway (Aug 18 2022 at 10:00):From: Makarius <makarius@sketis.net>
See the following example:
http://isabelle.in.tum.de/dist/library/FOL/ex/IffOracle.html
Makarius
Last updated: May 03 2024 at 08:18 UTC