I am trying to understand https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html and https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html and I have problems with the understanding the meaning of the basic items, namely:

types o, seq'

nonterminals seq, seqobj, seqcont?

Do these types and nonterminals have some "real world" counterparts? Sequent is represented by function [o, seq']=>seq', so, maybe o and seq' do not have any real world counterparts?

I am reading "Isabelle's Logics" (http://isabelle.in.tum.de/dist/Isabelle2016-1/doc/logics.pdf especially chapter 4), LNCS 828, Isabelle/Isar reference manual (especially 8.2 and 8.5 about mixfix notations and syntax definition), but I can not grasp the meaning of those symbols and therefor I can not move forward. Any guidance would be very helpful!

I am trying to implement monoidal logic http://www.sciencedirect.com/science/article/pii/S1570868314000573 as a object logic in Isabelle/HOL, but everything is so detached from the "real world" (how the mathematics is being done on paper).

  • 2
    $\begingroup$ Such theorem-provers have a VERY steep learning curve indeed. Perhaps I am just not clever enough, but I gave up and had to write my own proof assistant. It was great fun! You can download it at dcproof.com but it may not help much with monoidal logic. If you don't like the axioms I have built in, you can play around and introduce your own. $\endgroup$ – Dan Christensen Aug 22 '17 at 21:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.