Email Gateway (Aug 22 2022 at 21:09): Email Gateway (Aug 22 2022 at 21:09):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I would like to ask several questions with regard to the availability of
tools for the visualization of orders based on theorems stated in
Isabelle/HOL and certain other related questions:
1. Are there any tools already available for the visualization of orders
or relationships between predicates (apart from the locale_deps and
class_deps)? Are there any ongoing efforts dedicated to the development of
such tools?
2. Is it possible to extract (with ease) arbitrary subsets of the
diagrams produced by class_deps/locale_deps and add them to the formal
proof documents?
3. I would like to understand what is the policy on the inclusion of
external tools in the build process for the submission of articles to the
AFP. In particular, I would like to understand if it would be acceptable
for the build process to call any commands associated with graphviz.
Background
I sketched a graphviz-based snippet for the visualization of certain types
of partial orders in the form of the Hasse-like diagrams (more precisely,
at the moment, I allow the edges shown in such diagrams to form an
arbitrary subset of the edges of the traditional Hasse diagram for a given
ordered set) from theorems stated in Isabelle/HOL for a particular
application. I am thinking about whether it is worth taking this
development one step further and create a small package from it.
Unfortunately, it relies on graphviz and I am not certain whether this
could be allowed in the AFP submissions. Furthermore, before taking this
tool with any degree of seriousness, I would like to understand if anything
similar already exists or is being developed. I attached a couple of
screenshots taken from the formal proof documents amended with the diagrams
created by the (sketched) tool for a reference.
Thank you,
Mikhail Chekhov
example_1.png
example_2.png
Email Gateway (Aug 23 2022 at 09:02):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
This is a partial reply to one of my own old questions on the list:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-December/msg00058.html.
I thought that it may be worth making an attempt to resurrect this thread
in light of a recent paper by Clemens Ballarin for the Isabelle Workshop:
https://files.sketis.net/Isabelle_Workshop_2020/Isabelle_2020_paper_2.pdf.
This paper provides a positive answer to Question 2 from the thread that I
started. Thus, once again, I would like to thank the author (indeed, this
is the second time a publication from Clemens Ballarin provides an answer
to one of my questions on the list:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-April/msg00077.html
).
Undeniably, I am very interested in whether there exist any active projects
related to the extraction of diagrams from theories or auto-generation of
theories from diagrams (to the point of designing my own prototype for the
extraction of diagrams for one particular application area, not directly
related to locales), as well as finding the answers to Questions 1 and 3
from the aforementioned thread. Therefore, I would be very pleased to
receive any comments in relation to the aforementioned matters.
Kind Regards,
Mikhail Chekhov
Last updated: Apr 23 2024 at 08:19 UTC