I like the way you have equivalences and inferences defined as functions expr -> expr. But it seems those are not exposed via the user interface, or am I missing something?<p>Related: A few years ago I wrote a propositional logic parser in Dart [1] using a custom shunting yard parser and later as part of my bachelors thesis [2] another one [2] in javascript using PegJS.<p>[1] <a href="https://static.laszlokorte.de/logik/" rel="nofollow">https://static.laszlokorte.de/logik/</a> (source: <a href="https://github.com/laszlokorte/dart-logic" rel="nofollow">https://github.com/laszlokorte/dart-logic</a>)<p>[2] <a href="https://thesis.laszlokorte.de" rel="nofollow">https://thesis.laszlokorte.de</a><p>[3] <a href="https://thesis.laszlokorte.de/demo/logic-editor.html" rel="nofollow">https://thesis.laszlokorte.de/demo/logic-editor.html</a>