Symbolic propositional and predicate reasoning

New to Julia
1

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.

2

Just in case anyone else got stuck on this problem, a solution is to add “;” to end of input.
julia> dump(:(x))
Symbol x
julia> dump(:(x;))
Expr
head: Symbol block
args: Array{Any}((1,))
1: Symbol x

Similarly for literals 1,2,… true,… Now they can all be saved in Expr fields.