# Symbolic propositional and predicate reasoning

**URL:** https://discourse.julialang.org/t/symbolic-propositional-and-predicate-reasoning/80506
**Category:** New to Julia
**Tags:** metaprogramming
**Created:** [May 4, 2022, 8:18pm UTC](https://discourse.julialang.org/t/symbolic-propositional-and-predicate-reasoning/80506 "2022-05-04T20:18:33Z")
**Posts on this page:** 2
**Page:** 1

<div class="post-metadata">

### Author: ![davidstreader](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/davidstreader/32/35704_2.png) [@davidstreader](https://discourse.julialang.org/u/davidstreader)
#### Post date: [May 4, 2022, 8:18pm UTC](https://discourse.julialang.org/t/symbolic-propositional-and-predicate-reasoning/80506/1 "2022-05-04T20:18:33Z")

</div>

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.

---

<div class="post-metadata">

### Author: ![davidstreader](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/davidstreader/32/35704_2.png) [@davidstreader](https://discourse.julialang.org/u/davidstreader)
#### Post date: [May 18, 2022, 1:26am UTC](https://discourse.julialang.org/t/symbolic-propositional-and-predicate-reasoning/80506/2 "2022-05-18T01:26:14Z")

</div>

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.