Re: [isabelle] A (very) short Isabelle/HOL tutorial for the functional programmer



[I posted this earlier but it seems to have not appeared; since my posts on
this thread seem to be appearing I am reposting here]


Very new to Isabelle and theorem proving, so my questions may be stupid.
Please excuse!

I am interested in tools to help students with Dijkstra Scholten equational
logic
I find that there is one formalization in Maude:
https://www.ideals.illinois.edu/bitstream/handle/2142/11411/A%20Rewriting%20Decision%20Procedure%20for%20Dijkstra-Scholten's%20Syllogistic%20Logic%20with%20Complements.pdf?sequence=2
<https://www.ideals.illinois.edu/bitstream/handle/2142/11411/A%20Rewriting%20Decision%20Procedure%20for%20Dijkstra-Scholten%27s%20Syllogistic%20Logic%20with%20Complements.pdf?sequence=2>

Is redoing that in Isabelle a reasonable idea?

Regards
Rusi



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