[isabelle] Dijkstra Scholten Logic



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

Is redoing that in Isabelle a reasonable idea?

Regards
Rusi



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