{"id":96,"date":"2012-03-30T08:00:00","date_gmt":"2012-03-30T06:00:00","guid":{"rendered":"https:\/\/www.formalmind.com\/blog\/prob-logic-calculator\/"},"modified":"2022-04-11T18:58:55","modified_gmt":"2022-04-11T16:58:55","slug":"prob-logic-calculator","status":"publish","type":"post","link":"https:\/\/www.formalmind.com\/de\/blog\/prob-logic-calculator\/","title":{"rendered":"ProB Logikrechner"},"content":{"rendered":"<p>A first prototype of a <a href=\"http:\/\/www.stups.uni-duesseldorf.de\/ProB\/index.php5\/ProB_Logic_Calculator\">ProB Logic Calculator is now available online<\/a>. With it you can evaluate arbitrary expressions and predicates (using <a href=\"http:\/\/www.stups.uni-duesseldorf.de\/ProB\/index.php5\/Summary_of_B_Syntax\">B Syntax<\/a>). It is a great way to learn about B, predicate logic and set theory or even just to solve arithmetic constraints and puzzles.<\/p>\n<p><!--break--><\/p>\n<p>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&#8217;t work if you read this blog entry from your email client; in this case you have to go to <a href=\"https:\/\/www.formalmind.com\/en\/blog\/prob-logic-calculator\">https:\/\/www.formalmind.com\/en\/blog\/prob-logic-calculator<\/a>.<\/p>\n<p><iframe class=\"lazyload\" data-src=\"http:\/\/wyvern.cs.uni-duesseldorf.de:8080\/evalB\/embedded.html\" border=\"0\" scrolling=\"no\"  frameborder=\"0\" height=\"450\" width=\"640\"><\/p>\n<p>Your Browser does not suport IFrames.<\/p>\n<p><\/iframe><\/p>\n<p>Try and type in expressions like <tt>2**100<\/tt>, or <tt>{x|x*x=400}<\/tt> or predicates like <tt>x*x*x=15625<\/tt> in the above shell and see what happens.<\/p>\n<p>Short syntax guide for some of B&#8217;s constructs:<\/p>\n<ol>\n<li>conjunction <tt>P &amp; Q<\/tt>, disjunction <tt>P or Q<\/tt>, implication <tt>P =&gt; Q<\/tt>, equivalence <tt>P &lt;=&gt; Q<\/tt>, negation <tt>not(P)<\/tt>, existential quantification <tt>#x.(P)<\/tt>, universal quantification <tt>!x.(P=&gt;Q)<\/tt><\/li>\n<li>equality <tt>x=y<\/tt>, disequality <tt>x\/=y<\/tt><\/li>\n<li>arithmetic comparisons <tt>x &lt; y<\/tt>, <tt>x &gt; y<\/tt>, <tt>x &lt;= y<\/tt>, <tt>x &gt;= y<\/tt><\/li>\n<li>membership <tt>x:S<\/tt>, not membership, <tt>x\/:S<\/tt>, subset <tt>S&lt;:R<\/tt>, strict subset <tt>S &lt;&lt;: R<\/tt><\/li>\n<li>arithmetic operators <tt>x+y<\/tt>, <tt>x-y<\/tt>, <tt>x*y<\/tt>, <tt>x\/y<\/tt>, <tt>x mod y<\/tt>, <tt>x**y<\/tt><\/li>\n<li>mathematical integers <tt>INTEGER<\/tt>, mathematical natural numbers <tt>NATURAL<\/tt>, implementable integers <tt>INT<\/tt>, implementable naturals <tt>NAT<\/tt>, maximum implementable integer <tt>MAXINT<\/tt>, minimum implementable integer <tt>MININT<\/tt><\/li>\n<li>boolean values <tt>TRUE<\/tt>, <tt>FALSE<\/tt>, converting predicate to value <tt>bool(P)<\/tt><\/li>\n<li>strings <tt>\"...\"<\/tt>, set of all strings <tt>STRING<\/tt><\/li>\n<li>empty set <tt>{}<\/tt>, set enumeration <tt>{x,y,...}<\/tt>, comprehension set defined by predicate <tt>{x|P}<\/tt>, lambda abstraction <tt>%x.(P|E)<\/tt>, interval <tt>m..n<\/tt><\/li>\n<li>set union <tt>S \\\/ T<\/tt>, set intersection <tt>S \/\\ T<\/tt>, set difference <tt>S - T<\/tt>, power set <tt>POW(S)<\/tt>, Cartesian product <tt>S*T<\/tt>, cardinality of set <tt>card(S)<\/tt><\/li>\n<li>set of relations between two sets <tt>S &lt;-&gt; T<\/tt>, set of partial functions <tt>S +-&gt; T<\/tt>, set of total functions <tt>S --&gt; T<\/tt><\/li>\n<li>relational image <tt>r[S]<\/tt>, relational composition <tt>(r1 ; r2)<\/tt>, transitive closure <tt>closure1(r)<\/tt>, identity relation over a set <tt>id(S)<\/tt>, domain of a relation <tt>dom(r)<\/tt>, its range <tt>ran(r)<\/tt>, its inverse <tt>r~<\/tt>, relational overriding <tt>r1 &lt;+ r2<\/tt><\/li>\n<li>empty sequence <tt>[]<\/tt>, explicit sequence <tt>[x,y,...]<\/tt>, concatenation <tt>s1^s2<\/tt>, first element <tt>first(s)<\/tt>, tail <tt>tail(s)<\/tt>, prepend an element <tt>E-&gt;s<\/tt>, size of a sequence <tt>size(s)<\/tt><\/li>\n<li>sets of sequences over a set <tt>seq(S)<\/tt>, set of injective sequences <tt>iseq(S)<\/tt>, set of permutations <tt>perm(S)<\/tt><\/li>\n<\/ol>\n<p>More details can be found on our <a href=\"http:\/\/www.stups.uni-duesseldorf.de\/ProB\/index.php5\/Summary_of_B_Syntax\">B syntax summary page<\/a>. Note: statements (aka substitutions) and B machine construction elements cannot be used above; you must enter either a predicate or an expression.<\/p>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Ein erster Prototyp eines ProB Logic Calculators ist jetzt online verf\u00fcgbar. Mit ihm k\u00f6nnen Sie beliebige Ausdr\u00fccke und Pr\u00e4dikate (in B-Syntax) auswerten. Dies ist eine hervorragende M\u00f6glichkeit, etwas \u00fcber B, Pr\u00e4dikatenlogik und Mengenlehre zu lernen oder einfach nur arithmetische Einschr\u00e4nkungen und R\u00e4tsel zu l\u00f6sen. Eine alternative eingebettete ProB Logic Shell ist direkt\u2026<\/p>","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"single-no-separators","format":"standard","meta":{"_kadence_starter_templates_imported_post":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_kad_post_classname":"","footnotes":""},"categories":[13],"tags":[],"class_list":["post-96","post","type-post","status-publish","format-standard","hentry","category-blog"],"_links":{"self":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts\/96","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/comments?post=96"}],"version-history":[{"count":0,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts\/96\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/media?parent=96"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/categories?post=96"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/tags?post=96"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}