A first prototype of a ProB Logic Calculator is now available online. With it you can evaluate arbitrary expressions and predicates (using B Syntax). It is a great way to learn about B, predicate logic and set theory or even just to solve arithmetic constraints and puzzles.

An alternative embedded ProB Logic shell is directly embedded in this blog below. It processes single lines only, but has a formula history. It probably won’t work if you read this blog entry from your email client; in this case you have to go to https://www.formalmind.com/en/blog/prob-logic-calculator.

Try and type in expressions like 2**100, or {x|x*x=400} or predicates like x*x*x=15625 in the above shell and see what happens.

Short syntax guide for some of B’s constructs:

1. conjunction P & Q, disjunction P or Q, implication P => Q, equivalence P <=> Q, negation not(P), existential quantification #x.(P), universal quantification !x.(P=>Q)
2. equality x=y, disequality x/=y
3. arithmetic comparisons x < y, x > y, x <= y, x >= y
4. membership x:S, not membership, x/:S, subset S<:R, strict subset S <<: R
5. arithmetic operators x+y, x-y, x*y, x/y, x mod y, x**y
6. mathematical integers INTEGER, mathematical natural numbers NATURAL, implementable integers INT, implementable naturals NAT, maximum implementable integer MAXINT, minimum implementable integer MININT
7. boolean values TRUE, FALSE, converting predicate to value bool(P)
8. strings "...", set of all strings STRING
9. empty set {}, set enumeration {x,y,...}, comprehension set defined by predicate {x|P}, lambda abstraction %x.(P|E), interval m..n
10. set union S \/ T, set intersection S /\ T, set difference S - T, power set POW(S), Cartesian product S*T, cardinality of set card(S)
11. set of relations between two sets S <-> T, set of partial functions S +-> T, set of total functions S --> T
12. relational image r[S], relational composition (r1 ; r2), transitive closure closure1(r), identity relation over a set id(S), domain of a relation dom(r), its range ran(r), its inverse r~, relational overriding r1 <+ r2
13. empty sequence [], explicit sequence [x,y,...], concatenation s1^s2, first element first(s), tail tail(s), prepend an element E->s, size of a sequence size(s)
14. sets of sequences over a set seq(S), set of injective sequences iseq(S), set of permutations perm(S)

More details can be found on our B syntax summary page. Note: statements (aka substitutions) and B machine construction elements cannot be used above; you must enter either a predicate or an expression.