- OCaml (newer version)
$ echo "(a /\ b) => (b /\ a)" | ocaml ljt.ml
==========================
stdin
((a ∧ b) ⊃ (b ∧ a))
success!
• ----> ((a ∧ b) ⊃ (b ∧ a)) by ⊃R
• (a ∧ b) ----> (b ∧ a) by ∧R
• (a ∧ b) ----> b by ∧L
• b, a ----> b by init
• (a ∧ b) ----> a by ∧L
• a, b ----> a by initSome interesting unit tests:
$ ocaml ljt.ml test- The implementation of the formula parser is very naive and does not consider precedence and associativity.
Please add parentheses
(,)to specify them!
Standard ML implementation: https://github.com/ayberkt/sequents