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.

Your Browser does not suport IFrames.

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:

- 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)` - equality
`x=y`, disequality`x/=y` - arithmetic comparisons
`x < y`,`x > y`,`x <= y`,`x >= y` - membership
`x:S`, not membership,`x/:S`, subset`S<:R`, strict subset`S <<: R` - arithmetic operators
`x+y`,`x-y`,`x*y`,`x/y`,`x mod y`,`x**y` - mathematical integers
`INTEGER`, mathematical natural numbers`NATURAL`, implementable integers`INT`, implementable naturals`NAT`, maximum implementable integer`MAXINT`, minimum implementable integer`MININT` - boolean values
`TRUE`,`FALSE`, converting predicate to value`bool(P)` - strings
`"..."`, set of all strings`STRING` - empty set
`{}`, set enumeration`{x,y,...}`, comprehension set defined by predicate`{x|P}`, lambda abstraction`%x.(P|E)`, interval`m..n` - 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)` - set of relations between two sets
`S <-> T`, set of partial functions`S +-> T`, set of total functions`S --> T` - 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` - 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)` - 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.