Hi (big picture I am interested in reasoning about symbolic event based systems. Hence I am trying to build a Domain Specific Language similar to both TLA+ and CSP) I have found how to perform symbolic substitution and simplification using Symbolics.jl but this seems to exclude using Boolean terms. Am I correct in saying that Symbolics.jl has been designed for numeric computation and not for the evaluation of boolean expressions?

There are interesting packages like Rewrite.jl and MetaTheory.jl that give the ability to build the rewrites (and egraphs) so I see that i could implement something to evaluate logical terms but has this already been done? that is have the standard theories for Zero Ordered Logic or First Order Logic been implemented? if so where can I get them?

And can any one tell me Why

typeof(:(1+x)) == typeof(quote 1+x end) == typeof(quote 1 end) == Expr

But typeof(:(1)) == Int64 ? This took me - a rank beginner - many hours to sort out and I still cannot see what purpose this has.