In mathml: Translate R Expressions to 'MathML' and 'LaTeX'/'MathJax'

library(mathml)
rolog::consult(system.file(file.path("pl", "bussproofs.pl"), package="mathml"))

# 1. Excluded middle
term <- quote(ror('%>%'('', '%|%'(A, ~A)), rneg('%>%'('', '%,%'(A, ~A)), ax('%>%'(A, A), ''))))
math(term)

# 2. Dilemma 
term <- quote(rcond('%>%'('%->%'(('&'('%->%'(~A, B), '%->%'(A, B))), B)), land('%>%'('&'('%->%'(~A, B),'%->%'(A, B)), B), 
lcond('%>%'('%->%'('%->%'(~A, '%,%'(B, A)), B), B), 
rneg('%>%'('%->%'(A, B), '%,%'(~A, B)), 
lcond('%>%'('%->%'('%,%'(A, A), B), B), 
ax('%>%'(A, '%,%'(A, B)), ''), ax('%>%'('%,%'(B, A), B), ''))), 
ax('%>%'('%->%'('%,%'(B, A), B), B), '')))))
math(term)

# 3. Double negation
term <- quote(rbicond('%>%'('%<=>%'(~~A, A)), 
lneg('%>%'(~~A, A), 
rneg('%>%'('%,%'(~A, A)), 
ax('%>%'(A, A), ''))), 
rneg('%>%'(A, ~~A), 
lneg('%>%'('%,%'(~A, A), ''), 
ax('%>%'(A, A), '')))))
math(term)

# 4. Peirce's Law
term <- quote(rcond('%>%'('%->%'(('%->%'(('%->%'(A, B)), A)), A)), 
lcond('%>%'('%->%'(('%->%'(A, B)), A), A), 
rcond('%>%'('%->%'(A, '%,%'(B, A))), 
ax('%>%'(A, '%,%'(B, A)), '')), 
ax('%>%'(A, A), ''))))
math(term)

# 5. Dummett Formula
term <-quote(ror('%>%'('%|%'(('%->%'(A, B)), ('%->%'(B, A)))), 
rcond('%>%'('%->%'(A, '%->%'('%,%'(B, B), A))), 
rcond('%>%'('%->%'(A, '%->%'('%,%'(B, B), A))), 
ax('%>%'('%,%'(B, A), '%,%'(A, B)), '')))))
math(term)

# 6. Classical equivalence for negation
term <- quote(rbicond('%>%'('%<=>%'(('%->%'(~A, A)), A)), 
lcond('%>%'('%->%'(~A, A), A), 
rneg('%>%'('%,%'(~A, A)), 
ax('%>%'(A, A), '')), 
ax('%>%'(A, A), '')), 
rcond('%>%'(A, '%->%'(~A, A)), 
ax('%>%'('%,%'(~A, A), A), ''))))
math(term)

# 7. Classical De Morgan's Law
term <- quote(rcond('%>%'('%->%'(~('&'(A,B)), '%|%'(~A, ~B))), 
ror('%>%'(~('&'(A, B)), '%|%'(~A, ~B)), 
rneg('%>%'(~('&'(A, B)), '%,%'(~A, ~B)), 
rneg('%>%'('%,%'(A, ~('&'(A, B))), ~B), 
lneg('%>%'('%,%'('%,%'(B, A), ~('&'(A, B))), ''), 
rand('%>%'('%,%'(B, A), '&'(A, B)), 
ax('%>%'('%,%'(B, A), A), ''), 
ax('%>%'('%,%'(B, A), A), ''))))))))
math(term)

# 9. a
term <- quote(asq('%<%'(A), ''))
math(term)

# 10. a => b
term <- quote(rcond('%>%'('%->%'(A, B)), asq('%<%'(A, B), '')))
math(term)

# 11. (a | b) => (a & b)
term <- quote(rcond('%>%'('%->%'('%|%'(A, B), ('&'(A, B)))), 
rand('%>%'('%|%'(A, B), '&'(A, B)), 
lor('%>%'('%|%'(A, B), A), ax('%>%'(A, A), ''), 
    asq(B%<%A, '')), 
lor(A%|%B%>%B, asq('%<%'(A, B), ''), 
    ax('%>%'(B, B), '')))))
math(term)