Ein erster Prototyp eines Der ProB Logic Calculator ist jetzt online verfügbar. Mit ihm können Sie beliebige Ausdrücke und Prädikate auswerten (unter Verwendung B SyntaxEs ist eine großartige Möglichkeit, etwas über B, Prädikatenlogik und Mengenlehre zu lernen oder einfach nur arithmetische Einschränkungen und Rätsel zu lösen.
Eine alternative, eingebettete ProB Logic Shell ist direkt hier im Blog unten integriert. Sie verarbeitet nur einzelne Zeilen, verfügt aber über eine Formelhistorie. Sie wird wahrscheinlich nicht funktionieren, wenn Sie diesen Blogeintrag über Ihr E-Mail-Programm lesen. In diesem Fall müssen Sie zu https://www.formalmind.com/en/blog/prob-logic-calculator.
Versuchen Sie, Ausdrücke einzugeben wie 2**100, oder {x|x*x=400} oder Prädikate wie x*x*x=15625 in der obigen Shell und sehen Sie, was passiert.
Kurze Syntaxanleitung für einige von B's Konstrukten:
- Konjunktion P & Q, oder P oder Q, Implikation P => Q, Gleichwertigkeit P genau dann, wenn Q, Negation nicht(P), existenzielles Quantifizieren #x.(P), universelle Quantifizierung !x.(P=>Q)
- Gleichheit x=y, Ungleichheit x /= y
- arithmetische Vergleiche x < y, x > y, x kleiner oder gleich y, x ist größer oder gleich y
- Mitgliedschaft x:S, nicht Mitgliedschaft, x/:S, Teilmenge S<:R, echte Teilmenge S <<: R
- arithmetische Operatoren x+y, x-y, x*y, x/y, x modulo y, x hoch y
- mathematische ganze Zahlen GANZE ZAHL, mathematische natürliche Zahlen NATURALE, implementierbare ganze Zahlen INT, implementierbare Natürlichkeit NAT, maximal implementierbare Ganzzahl MAXINT, minimal implementierbare ganze Zahl Mindest
- boolesche Werte WAHR, FALSCH, Umwandlung von Prädikat in Wert bool(P)
- Zeichenketten "...", Menge aller Zeichenketten Zeichenkette
- leere Menge {}, Sammlungsaufzählung {x,y,...}, ,comprehension set defined by predicate {x|P}, Lambda-Abstraktion %x.(P|E), Intervall m..n
- Mengenvereinigung S \/ T, Schnittelement S ∩ T, Mengendifferenz S - T, Potenzmenge POW(S), kartesisches Produkt S*T, Kardinalität einer Menge Karte(n)
- Menge von Relationen zwischen zwei Mengen S T, Menge von partiellen Funktionen S +-> T, Menge aller Funktionen S --> T
- relationales Bild r[S], relationale Komposition (r1 ; r2), Transitive Hülle Schließung1(r), Identitätsrelation über einer Menge id(S), Definitionsbereich einer Relation Definitionsbereich von r, seine Reichweite ran, seine Umkehrung r~, relationale Überschreibung r1 <+ r2
- leere Sequenz [], explizite Sequenz [x,y,...], Verkettung s1 hoch s2, erstes Element erstens, Schwanz Schwanz(e), ein Element voranstellen E->s, Größe einer Sequenz Größe(n)
- Mengen von Folgen über einer Menge seq(S), Menge injektiver Folgen iseq(S), Menge von Permutationen perm(S)
Weitere Details finden Sie auf unserer B Syntax-Zusammenfassungsseite. Beachten Sie: Aussagen (auch Substitutionen) und Konstruktionselemente der B-Maschine dürfen nicht oben verwendet werden. Sie müssen entweder ein Prädikat oder einen Ausdruck eingeben.
