10145:, another variant of modal logic sharing many common features with dynamic logic, differs from all of the above-mentioned logics by being what Pnueli has characterized as an "endogenous" logic, the others being "exogenous" logics. By this Pnueli meant that temporal logic assertions are interpreted within a universal behavioral framework in which a single global situation changes with the passage of time, whereas the assertions of the other logics are made externally to the multiple actions about which they speak. The advantage of the endogenous approach is that it makes no fundamental assumptions about what causes what as the environment changes with time. Instead a temporal logic formula can talk about two unrelated parts of a system, which because they are unrelated tacitly evolve in parallel. In effect ordinary logical conjunction of temporal assertions is the concurrent composition operator of temporal logic. The simplicity of this approach to concurrency has resulted in temporal logic being the modal logic of choice for reasoning about concurrent systems with its aspects of synchronization, interference, independence,
9557:
formalize the intuitive notions of truth and validity, which in turn permit the notions of soundness and completeness to be defined for axiom systems. An inference rule is sound when validity of its premises implies validity of its conclusion. An axiom system is sound when all its axioms are valid and its inference rules are sound. An axiom system is complete when every valid formula is derivable as a theorem of that system. These concepts apply to all
3853:
suffice also for dynamic logic as the only primitive rules it needs, as noted above. However, as usual in logic, many more rules can be derived from these with the help of the axioms. An example instance of such a derived rule in dynamic logic is that if kicking a broken TV once can't possibly fix
10136:
Hoare logic, algorithmic logic, weakest preconditions, and dynamic logic are all well suited to discourse and reasoning about sequential behavior. Extending these logics to concurrent behavior however has proved problematic. There are various approaches but all of them lack the elegance of the
9556:
semantics or Kripke structures. This semantics carries over naturally to dynamic logic by interpreting worlds as states of a computer in the application to program verification, or states of our environment in applications to linguistics, AI, etc. One role for possible world semantics is to
9901:
who showed that PDL was decidable in deterministic exponential time. In 1977, Krister
Segerberg proposed a complete axiomatization of PDL, namely any complete axiomatization of modal logic K together with axioms A1–A6 as given above. Completeness proofs for Segerberg's axioms were found by
4171:
means that if the TV is broken, then after kicking it zero or more times it will still be broken. For if not, then after the second-to-last kick the TV would be in a state where kicking it once more would fix it, which the premise claims can never happen under any circumstances.
10124:, weakest liberal precondition. Those logics however made no connection with either modal logic, Kripke semantics, regular expressions, or the calculus of binary relations. Dynamic logic therefore can be viewed as a refinement of algorithmic logic and
2796:
2731:
2949:
2865:
8040:
7519:
7395:
5040:
is an expression built from constants and variables with whatever operations are provided by the language, such as addition and multiplication. The Hoare axiom for assignment is not given as a single axiom but rather as an axiom schema.
9848:. PDL blends the ideas behind propositional logic and dynamic logic by adding actions while omitting data; hence the terms of PDL are actions and propositions. The TV example above is expressed in PDL whereas the next example involving
7680:
3320:
Box and diamond are entirely symmetric with regard to which one takes as primitive. An alternative axiomatization would have been to take the theorems T1–T6 as axioms, from which we could then have derived A1–A6 as theorems.
95:
6214:
6855:
8612:
2586:
1445:
932:
880:
4880:
8541:
8884:
9542:
9233:
2662:
9378:
5550:
8239:
5401:
5105:
2354:
5748:
5474:
10122:
8457:
1863:
1729:
10051:
4473:
however must be true. But this could happen in any situation where the TV is broken but can be revived with two kicks. The implication fails (is not valid) because it only requires that
2623:
10315:, "Dynamic Logic", In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, chapter 10, pages 497-604. Reidel, Dordrecht, 1984.
4621:
377:
9573:
has two types of terms, respectively assertions and data. As can be seen from the examples above, dynamic logic adds a third type of term denoting actions. The dynamic logic assertion
8725:
3468:. However the dynamic nature of dynamic logic moves this distinction out of the realm of abstract axiomatics into the common-sense experience of situations in flux. The inference rule
4307:
1944:
7207:
4234:
3957:
9085:
8490:
1794:
1660:
736:
4807:
3021:
582:
8917:
8667:
1197:
7083:
8241:
without impacting any of this, the other direction being provable from A5, from which we see that if the antecedent of A6 does happen to be false somewhere, then the consequent
3813:
175:
211:
7164:
2738:
337:
9815:
9626:
9403:
9340:
7708:
5633:
5304:
3503:
3422:
1503:
7891:
7007:
6942:
6686:
6296:
5945:
5213:
5138:
2669:
976:
954:
9962:
9760:
9045:
8995:
8945:
8753:
5886:
5661:
5599:
1059:
9999:
9880:
9732:
6001:
4936:
4743:
4545:
4508:
4384:
4344:
4169:
4102:
4034:
3994:
3687:
3606:
3350:
2872:
1587:
1527:
482:
7786:
5279:
5235:
5160:
9431:
7757:
4994:
4129:
2803:
1554:
1474:
1381:
1272:
309:
9676:
8138:
7921:
7400:
1121:
1091:
237:
8396:
8345:
8298:
437:
10082:
9698:
9648:
9277:
9255:
9192:
9170:
9148:
9107:
9017:
8967:
8819:
8797:
8775:
8689:
8634:
8371:
8320:
8273:
8160:
8110:
8084:
8062:
7913:
7860:
7830:
7808:
7730:
7566:
7544:
7261:
7127:
7105:
6877:
6622:
6600:
6578:
6516:
6494:
6472:
6450:
6428:
6406:
6340:
6318:
6258:
6236:
6045:
6023:
5967:
5914:
5858:
5836:
5814:
5792:
5770:
5690:
5326:
5257:
5182:
5038:
5016:
4958:
4902:
4709:
4687:
4665:
4643:
4471:
4440:
4406:
4065:
3896:
3874:
3835:
3740:
3709:
3650:
3628:
3569:
3547:
3525:
3466:
3444:
3394:
3372:
3315:
3293:
3271:
3249:
3227:
3205:
3183:
3155:
3133:
3111:
3089:
3067:
3045:
2526:
2492:
2470:
2448:
2426:
2404:
2382:
2298:
2276:
2254:
2232:
2210:
2188:
2164:
2142:
2120:
2098:
2076:
2054:
2030:
1994:
1972:
1621:
1346:
1320:
1298:
1245:
1223:
1165:
1143:
1031:
1009:
981:
Dynamic logic permits compound actions built up from smaller actions. While the basic control operators of any programming language could be used for this purpose,
824:
802:
780:
758:
705:
683:
661:
639:
617:
526:
504:
459:
9315:
7256:
6556:
6384:
4779:
2993:
554:
262:
8162:
is not a natural number, then the antecedent is false and so A6 remains true regardless of the truth of the consequent. We could strengthen A6 to an equivalence
10325:, and Jerzy Tiuryn, "Dynamic Logic", In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 4: pages 99-217. Kluwer, 2nd edition, 2002.
9477:
9457:
7579:
286:
138:
10128:
that connects them up to the axiomatics and Kripke semantics of modal logic as well as to the calculi of binary relations and regular expressions.
56:
8997:
at the end blocks the performer from terminating the iteration prematurely, but as soon as it becomes false, further iterations of the body
6050:
10306:
6691:
10178:
8552:
2539:
1398:
885:
833:
4812:
8500:
5476:. Such an axiom schema allows infinitely many axioms having a common form to be written as a finite expression connoting that form.
8831:
9482:
9197:
3324:
The difference between implication and inference is the same in dynamic logic as in any other logic: whereas the implication
2630:
827:
9345:
5482:
9821:
is derived from first-order logic by omitting data terms and reasons only about abstract propositions, which may be simple
8165:
5331:
5049:
10217:
17:
2305:
10372:
9882:
is in first-order dynamic logic. PDL is to (first-order) dynamic logic as propositional logic is to first-order logic.
5695:
5406:
1391:
These operators can be axiomatized in dynamic logic as follows, taking as already given a suitable axiomatization of
10087:
8410:
1801:
1667:
10016:
10125:
2594:
4553:
10283:
10253:
8694:
4239:
1870:
7169:
4178:
3901:
9058:
8464:
1736:
1628:
710:
10377:
4784:
2998:
559:
342:
32:
8889:
8639:
1170:
10146:
7012:
3745:
151:
2791:{\displaystyle \langle a\mathbin {;} b\rangle p\leftrightarrow \langle a\rangle \langle b\rangle p\,\!}
268:(and, or, and not). The action logic is expressive enough to encode programs. For an arbitrary program
100:
which states that if the ground is currently dry and it rains, then afterwards the ground will be wet.
10183:
2726:{\displaystyle \langle a\cup b\rangle p\leftrightarrow \langle a\rangle p\lor \langle b\rangle p\,\!}
188:
7132:
10351:
9886:
9765:
9576:
9383:
9320:
7688:
5604:
5284:
3471:
3399:
2944:{\displaystyle \langle a*\rangle p\to p\lor \langle a*\rangle (\neg p\land \langle a\rangle p)\,\!}
1479:
7865:
6947:
6882:
6630:
6270:
5919:
5187:
5112:
959:
937:
9933:
9737:
9022:
8972:
8922:
8730:
5863:
5638:
5555:
2860:{\displaystyle \langle a*\rangle p\leftrightarrow p\lor \langle a\rangle \langle a*\rangle p\,\!}
1036:
399:
10245:
10239:
9967:
9851:
9703:
9544:. Hence we must either reject Dijkstra's argument or hold that the * operator is not effective.
9459:
to an arbitrary positive integer. However, in dynamic logic with assignment and the * operator,
8035:{\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}
7514:{\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}
5972:
4907:
4714:
4513:
4476:
4349:
4312:
4134:
4070:
3999:
3962:
3655:
3574:
3327:
1559:
1508:
464:
9822:
7762:
5891:
5262:
5218:
5143:
2495:
317:
9408:
7735:
7390:{\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i)))\to \forall i\Phi (n+i)\,\!}
4971:
4107:
1536:
1456:
1359:
1250:
294:
10270:
9907:
9653:
8115:
6627:
One way of dealing with the opacity of modalities is to eliminate them. To this end, expand
1096:
1068:
216:
9926:
in 1974 in notes for a class on program verification as an approach to assigning meaning to
9405:. That is, first-order logic can be understood as the dynamic logic of programs of the form
8376:
8325:
8278:
419:
265:
10367:
10056:
9681:
9631:
9260:
9238:
9175:
9153:
9112:
9090:
9000:
8950:
8802:
8780:
8758:
8672:
8617:
8354:
8303:
8256:
8143:
8093:
8067:
8045:
7896:
7843:
7813:
7791:
7713:
7549:
7527:
7110:
7088:
6860:
6605:
6583:
6561:
6499:
6477:
6455:
6433:
6411:
6389:
6323:
6301:
6241:
6219:
6028:
6006:
5950:
5897:
5841:
5819:
5797:
5775:
5753:
5673:
5309:
5240:
5165:
5021:
4999:
4941:
4885:
4692:
4670:
4648:
4626:
4445:
4411:
4389:
4039:
3879:
3857:
3818:
3714:
3692:
3633:
3611:
3552:
3530:
3508:
3449:
3427:
3377:
3355:
3298:
3276:
3254:
3232:
3210:
3188:
3166:
3138:
3116:
3094:
3072:
3050:
3028:
2509:
2475:
2453:
2431:
2409:
2387:
2365:
2281:
2259:
2237:
2215:
2193:
2171:
2147:
2125:
2103:
2081:
2059:
2037:
2013:
1977:
1955:
1595:
1329:
1303:
1281:
1228:
1206:
1148:
1126:
1014:
992:
807:
785:
763:
741:
688:
666:
644:
622:
591:
509:
487:
442:
9282:
7675:{\displaystyle (\Phi (0)\land \forall i(\Phi (i)\to \Phi (i+1)))\to \forall i\Phi (i)\,\!}
7397:. The remaining modality can now be eliminated with one more use of Hoare's axiom to give
7212:
6521:
6349:
5816:
is 8 to begin with, or 6.5, whence this proposition is not a theorem of dynamic logic. If
4756:
2970:
531:
242:
8:
9818:
387:
10188:
9841:
9462:
9442:
8112:
is a natural number, then the antecedent of the main implication of A6 holds, but then
5664:
986:
271:
114:
10279:
10249:
10006:
9570:
7569:
3898:
for the proposition that the TV is broken, dynamic logic expresses this inference as
390:
of programs, dynamic logic has been applied to describe complex behaviors arising in
10214:
6047:. The first two of these three instantiations are straightforward, converting A6 to
4104:
means that if the TV is broken, then after kicking it once it will still be broken.
4067:
is that it is guaranteed that after kicking the TV, it is broken. Hence the premise
9558:
6343:
585:
44:
10010:
9436:
7810:. The importance of keeping this typing information straight becomes apparent if
2588:
permits the derivation of the following six theorems corresponding to the above:
506:
is possibly the case. Dynamic logic extends this by associating to every action
10173:
10168:
10142:
10002:
9845:
9840:
Propositional dynamic logic, or PDL, was derived from dynamic logic in 1977 by
9553:
9439:
claimed to show the impossibility of a program that sets the value of variable
2357:
982:
414:
379:
encodes the correctness of the program, making dynamic logic more general than
6264:
of modal logic in the case when a modality can interfere with a substitution.
4131:
denotes the action of kicking the TV zero or more times. Hence the conclusion
10361:
10302:
9923:
9898:
9885:
Fischer and Ladner showed in their 1977 paper that PDL satisfiability was of
7840:, for any of which A6 is perfectly valid as an axiom. As a case in point, if
4510:
hold now, whereas the inference succeeds (is sound) because it requires that
312:
8799:
is true the performer of the action can only take the left branch, and when
8042:, is just as valid, that is, true in every state regardless of the value of
10335:
10322:
10305:, "Semantical Considerations on Floyd-Hoare Logic", Proc. 17th Annual IEEE
10205:
9911:
9479:
can be set to an arbitrary positive integer with the dynamic logic program
5860:
is at most 7 to begin with, that is, it is just a roundabout way of saying
1449:
289:
9019:
are blocked and the performer then has no choice but to exit via the test
10341:
10318:
10312:
10201:
10163:
10138:
9927:
9825:
or atoms or compound propositions built with such logical connectives as
5838:
is of type integer however, then this proposition is true if and only if
1392:
410:
391:
380:
264:(doing one action zero or more times). The proposition language supports
90:{\displaystyle {\text{The ground is dry}}\to {\text{The ground is wet}},}
40:
7524:
With the opaque modalities now out of the way, we can safely substitute
16:
For the subject in digital electronics also known as clocked logic, see
9903:
2428:
after that performance entails its truth after one more performance of
1395:
including such axioms for modal operators as the above-mentioned axiom
395:
28:
6209:{\displaystyle (\Phi (n)\land (\Phi (n)\to \Phi (n)))\to \Phi (n)\,\!}
2953:
T1 asserts the impossibility of bringing anything about by performing
2010:
acts as the identity function on propositions, that is, it transforms
10005:
in its own right. The system parallels
Andrzej Salwicki's system of
6850:{\displaystyle \Phi (n)\land \Phi (n)\land \Phi (n)\land \ldots \,\!}
3854:
it, then repeatedly kicking it can't possibly fix it either. Writing
4809:
have the same meaning. Hence the above proposition is equivalent to
4689:
must be greater or equal to 4. In the case of deterministic actions
3630:
at the present moment is no guarantee of its truth after performing
10150:
9890:
2302:
A5 is the evident result of applying A2, A3 and A4 to the equation
8607:{\displaystyle (p?\mathbin {;} a)\cup (\neg p?\mathbin {;} b)\,\!}
6496:
will result in its executing in a different environment. However,
10278:. Warszawa & Boston: PWN & D. Reidel Publ. p. 372.
9894:
2581:{\displaystyle p\leftrightarrow \neg \langle a\rangle \neg p\,\!}
1440:{\displaystyle p\leftrightarrow \neg \langle a\rangle \neg p\,\!}
1326:
does nothing and does not terminate, whereas the constant action
927:{\displaystyle \langle a\rangle p\leftrightarrow \neg \neg p\,\!}
875:{\displaystyle p\leftrightarrow \neg \langle a\rangle \neg p\,\!}
7710:
should be understood as ranging over the natural numbers, where
4875:{\displaystyle (x\geq 3)\to \langle x:=x+1\rangle (x\geq 4)\,\!}
10208:, and Jerzy Tiuryn, "Dynamic Logic". MIT Press, 2000 (450 pp).
8536:{\displaystyle \langle p?\rangle q\leftrightarrow p\land q\,\!}
8351:, changing nothing while allowing the action to move on. When
5894:
can be obtained as the instance of A6 in which the proposition
7209:. This whole reduction should be applied to both instances of
6518:
itself is not a rigid designator with respect to the modality
8879:{\displaystyle ({p?\mathbin {;} a)*}\mathbin {;} \neg p?\,\!}
7573:
6386:, meaning that it is the same proposition after incrementing
24:
7918:, then axiom A6 after the first two substitutions, that is,
4309:
is not valid because we can easily find situations in which
5552:
of A7 allows us to calculate mechanically that the example
2004:
abstracts the essence of the action of hell freezing over.)
9537:{\displaystyle (x\mathbin {:=} 0)\mathbin {;} (x:=x+1){*}}
8140:
is also a natural number so the consequent also holds. If
3505:, for example, is sound because its premise asserts that
989:
operators are a good match to modal logic. Given actions
934:, analogously to the relationship between the universal (
10013:'s notion of weakest-precondition predicate transformer
9228:{\displaystyle \langle x\mathbin {:=} {?}\rangle p\,\!}
5794:
equal to 7. This of course is not always true, e.g. if
5670:
An example illustrating assignment in combination with
2657:{\displaystyle \langle 1\rangle p\leftrightarrow p\,\!}
9373:{\displaystyle \langle x\mathbin {:=} {?}\rangle \,\!}
9317:
thus has the same meaning as the universal quantifier
9050:
5545:{\displaystyle (x\geq 4)\leftrightarrow x+1\geq 4\,\!}
1300:
zero or more times, sequentially. The constant action
10090:
10059:
10019:
9970:
9936:
9854:
9768:
9740:
9706:
9684:
9656:
9634:
9579:
9552:
Modal logic is most commonly interpreted in terms of
9485:
9465:
9445:
9411:
9386:
9348:
9323:
9285:
9263:
9241:
9200:
9178:
9156:
9115:
9093:
9061:
9025:
9003:
8975:
8953:
8925:
8892:
8834:
8805:
8783:
8761:
8733:
8697:
8675:
8642:
8620:
8555:
8503:
8467:
8413:
8379:
8357:
8328:
8306:
8281:
8259:
8168:
8146:
8118:
8096:
8070:
8048:
7924:
7899:
7868:
7846:
7816:
7794:
7765:
7738:
7716:
7691:
7582:
7552:
7530:
7403:
7264:
7215:
7172:
7135:
7113:
7091:
7015:
6950:
6885:
6863:
6694:
6633:
6608:
6586:
6564:
6524:
6502:
6480:
6458:
6436:
6414:
6392:
6352:
6326:
6304:
6273:
6244:
6222:
6053:
6031:
6009:
5975:
5953:
5922:
5900:
5866:
5844:
5822:
5800:
5778:
5756:
5698:
5676:
5641:
5607:
5558:
5485:
5409:
5334:
5312:
5287:
5265:
5243:
5221:
5190:
5168:
5146:
5115:
5052:
5024:
5002:
4974:
4944:
4910:
4888:
4815:
4787:
4759:
4717:
4695:
4673:
4651:
4629:
4556:
4550:
An example of a valid implication is the proposition
4516:
4479:
4448:
4414:
4392:
4352:
4315:
4242:
4181:
4137:
4110:
4073:
4042:
4002:
3965:
3904:
3882:
3860:
3821:
3748:
3717:
3695:
3658:
3636:
3614:
3577:
3555:
3533:
3511:
3474:
3452:
3430:
3402:
3380:
3358:
3330:
3301:
3279:
3257:
3235:
3213:
3191:
3169:
3141:
3119:
3097:
3075:
3053:
3031:
3001:
2973:
2875:
2806:
2741:
2672:
2633:
2597:
2542:
2512:
2478:
2456:
2434:
2412:
2390:
2368:
2308:
2284:
2262:
2240:
2218:
2196:
2174:
2150:
2128:
2106:
2084:
2062:
2040:
2016:
1980:
1958:
1873:
1804:
1739:
1670:
1631:
1598:
1562:
1539:
1511:
1482:
1459:
1401:
1362:
1332:
1306:
1284:
1253:
1231:
1209:
1173:
1151:
1129:
1099:
1071:
1039:
1017:
995:
962:
940:
888:
836:
810:
788:
766:
744:
713:
691:
669:
647:
625:
594:
562:
534:
512:
490:
467:
445:
422:
345:
320:
297:
274:
245:
219:
191:
154:
117:
59:
10268:
9564:
9380:
similarly corresponds to the existential quantifier
8234:{\displaystyle p\land (p\to p)\leftrightarrow p\,\!}
5750:. This asserts that it is possible, by incrementing
5396:{\displaystyle (x=y^{2})\leftrightarrow e=y^{2}\,\!}
5100:{\displaystyle \Phi (x)\leftrightarrow \Phi (e)\,\!}
50:
A simple example of a statement in dynamic logic is
103:The syntax of dynamic logic contains a language of
10116:
10076:
10045:
9993:
9956:
9897:in the worst case. This gap was closed in 1978 by
9874:
9809:
9754:
9726:
9692:
9670:
9642:
9620:
9536:
9471:
9451:
9425:
9397:
9372:
9334:
9309:
9271:
9249:
9227:
9186:
9164:
9142:
9101:
9079:
9039:
9011:
8989:
8961:
8939:
8911:
8878:
8813:
8791:
8769:
8747:
8719:
8683:
8661:
8628:
8606:
8535:
8484:
8451:
8390:
8365:
8339:
8314:
8292:
8267:
8233:
8154:
8132:
8104:
8078:
8056:
8034:
7907:
7885:
7854:
7824:
7802:
7780:
7751:
7724:
7702:
7674:
7560:
7538:
7513:
7389:
7250:
7201:
7158:
7121:
7099:
7077:
7001:
6936:
6871:
6849:
6680:
6616:
6594:
6580:, it denotes 4 after. So we can't just substitute
6572:
6550:
6510:
6488:
6466:
6444:
6422:
6400:
6378:
6334:
6312:
6290:
6252:
6230:
6208:
6039:
6017:
5995:
5961:
5939:
5908:
5880:
5852:
5830:
5808:
5786:
5764:
5742:
5684:
5655:
5627:
5601:encountered a few paragraphs ago is equivalent to
5593:
5544:
5468:
5395:
5320:
5298:
5273:
5251:
5229:
5207:
5176:
5154:
5132:
5099:
5032:
5010:
4988:
4952:
4930:
4896:
4874:
4801:
4773:
4737:
4703:
4681:
4659:
4645:is greater or equal to 3, then after incrementing
4637:
4615:
4547:hold in all situations, not just the present one.
4539:
4502:
4465:
4434:
4400:
4378:
4338:
4301:
4228:
4163:
4123:
4096:
4059:
4028:
3988:
3951:
3890:
3868:
3829:
3807:
3734:
3703:
3681:
3644:
3622:
3600:
3563:
3541:
3519:
3497:
3460:
3438:
3416:
3388:
3366:
3344:
3309:
3287:
3265:
3243:
3221:
3199:
3177:
3149:
3127:
3105:
3083:
3061:
3039:
3015:
2987:
2943:
2859:
2790:
2725:
2656:
2617:
2580:
2520:
2486:
2464:
2442:
2420:
2398:
2376:
2349:{\displaystyle a{*}=1\cup a{\mathbin {;}}a{*}\,\!}
2348:
2292:
2270:
2248:
2226:
2204:
2182:
2158:
2136:
2114:
2092:
2070:
2048:
2024:
1988:
1966:
1938:
1857:
1788:
1723:
1654:
1615:
1581:
1548:
1521:
1497:
1468:
1439:
1375:
1340:
1314:
1292:
1266:
1239:
1217:
1191:
1159:
1137:
1115:
1085:
1053:
1025:
1003:
970:
948:
926:
874:
818:
796:
774:
752:
730:
699:
677:
655:
633:
611:
576:
548:
520:
498:
476:
453:
431:
371:
331:
303:
280:
256:
231:
205:
169:
132:
89:
10113:
10073:
10042:
9990:
9953:
9871:
9806:
9751:
9723:
9689:
9667:
9639:
9617:
9422:
9394:
9369:
9331:
9306:
9268:
9246:
9224:
9183:
9161:
9139:
9098:
9076:
9036:
9008:
8986:
8958:
8936:
8908:
8875:
8810:
8788:
8766:
8744:
8716:
8680:
8658:
8625:
8603:
8532:
8481:
8448:
8387:
8362:
8336:
8311:
8289:
8264:
8230:
8151:
8129:
8101:
8075:
8053:
8031:
7904:
7882:
7851:
7821:
7799:
7777:
7748:
7721:
7699:
7671:
7557:
7535:
7510:
7386:
7247:
7198:
7155:
7118:
7096:
7074:
6998:
6933:
6868:
6846:
6677:
6613:
6591:
6569:
6547:
6507:
6485:
6463:
6441:
6419:
6397:
6375:
6331:
6309:
6287:
6249:
6227:
6216:. However, the ostensibly simple substitution of
6205:
6036:
6014:
5992:
5958:
5936:
5905:
5877:
5849:
5827:
5805:
5783:
5761:
5739:
5681:
5652:
5624:
5590:
5541:
5465:
5392:
5317:
5295:
5270:
5248:
5226:
5204:
5173:
5151:
5129:
5096:
5029:
5007:
4985:
4949:
4927:
4893:
4871:
4798:
4770:
4734:
4700:
4678:
4656:
4634:
4612:
4536:
4499:
4462:
4431:
4397:
4375:
4335:
4298:
4225:
4160:
4120:
4093:
4056:
4025:
3985:
3948:
3887:
3865:
3826:
3804:
3731:
3700:
3678:
3641:
3619:
3597:
3560:
3538:
3516:
3494:
3457:
3435:
3413:
3385:
3363:
3341:
3306:
3284:
3262:
3240:
3218:
3196:
3174:
3163:T6 asserts that if it is possible to bring about
3146:
3124:
3102:
3080:
3058:
3036:
3012:
2984:
2940:
2856:
2787:
2722:
2653:
2614:
2577:
2517:
2483:
2461:
2439:
2417:
2395:
2373:
2345:
2289:
2267:
2245:
2223:
2201:
2179:
2155:
2133:
2111:
2089:
2067:
2045:
2021:
1985:
1963:
1935:
1854:
1785:
1720:
1651:
1612:
1436:
1372:
1337:
1311:
1289:
1263:
1236:
1214:
1188:
1156:
1134:
1112:
1082:
1050:
1022:
1000:
967:
945:
923:
871:
815:
793:
771:
749:
727:
696:
674:
652:
630:
608:
573:
545:
517:
495:
450:
111:(like "it rains"). The core modal constructs are
10359:
10244:. Englewood Cliffs: Prentice-Hall Inc. pp.
10001:. The approach was later published in 1976 as a
6260:is not so simple as it brings out the so-called
5743:{\displaystyle \langle (x:=x+1)*\rangle x=7\,\!}
5469:{\displaystyle (b=c+x)\leftrightarrow b=c+e\,\!}
5162:containing zero or more instances of a variable
4386:does not. In any such counterexample situation,
2472:must remain true no matter how often we perform
9087:denotes the nondeterministic action of setting
4968:The general form of an assignment statement is
4904:is greater or equal to 3 then after performing
830:to each other, which means they are related by
185:holds. The action language supports operations
10336:Semantical Considerations on Floyd-Hoare Logic
8253:Dynamic logic associates to every proposition
2384:holds now, and no matter how often we perform
10117:{\displaystyle \operatorname {wlp} (a,p)\,\!}
8614:. This action expresses a guarded choice: if
8452:{\displaystyle q\leftrightarrow (p\to q)\,\!}
7166:, then simplify this infinite conjunction to
6320:, we were thinking of the proposition symbol
3840:
3273:is (still) false but one more performance of
2967:is both deterministic and terminating whence
1858:{\displaystyle p\leftrightarrow p\land p\,\!}
1724:{\displaystyle p\leftrightarrow p\land p\,\!}
239:(doing one action or another), and iteration
107:(like "the ground is dry") and a language of
10307:Symposium on Foundations of Computer Science
10131:
10046:{\displaystyle \operatorname {wp} (a,p)\,\!}
9946:
9940:
9365:
9349:
9217:
9201:
8513:
8504:
8477:
8468:
6452:is still the same action after incrementing
5726:
5699:
4852:
4834:
4794:
4788:
3608:is not valid, however, because the truth of
3251:repeatedly to bring about a situation where
3008:
3002:
2930:
2924:
2909:
2900:
2885:
2876:
2849:
2840:
2837:
2831:
2816:
2807:
2780:
2774:
2771:
2765:
2756:
2742:
2715:
2709:
2700:
2694:
2685:
2673:
2640:
2634:
2607:
2601:
2567:
2561:
1426:
1420:
895:
889:
861:
855:
720:
714:
569:
563:
177:, which states that after performing action
161:
155:
140:, which states that after performing action
10179:Temporal logic in finite-state verification
9547:
6430:may impact its truth. Likewise, the action
3527:holds at all times, whence no matter where
2618:{\displaystyle \neg \langle 0\rangle p\,\!}
1948:Axiom A1 makes the empty promise that when
7685:One subtlety we glossed over here is that
5328:. For example, we may instantiate A7 with
5281:, i.e. not bound by some quantifier as in
4711:that are guaranteed to terminate, such as
4616:{\displaystyle (x\geq 3)\to (x\geq 4)\,\!}
10112:
10072:
10041:
9989:
9952:
9870:
9805:
9750:
9722:
9688:
9666:
9638:
9616:
9421:
9393:
9368:
9330:
9305:
9267:
9245:
9223:
9182:
9160:
9138:
9097:
9075:
9035:
9007:
8985:
8957:
8935:
8907:
8874:
8809:
8787:
8765:
8743:
8720:{\displaystyle \neg p?\mathbin {;} b\,\!}
8715:
8679:
8657:
8624:
8602:
8531:
8480:
8447:
8386:
8361:
8335:
8310:
8288:
8263:
8229:
8150:
8128:
8100:
8074:
8052:
8030:
7903:
7881:
7850:
7820:
7798:
7776:
7747:
7720:
7698:
7670:
7556:
7534:
7509:
7385:
7246:
7197:
7154:
7117:
7095:
7073:
6997:
6932:
6867:
6845:
6676:
6612:
6590:
6568:
6546:
6506:
6484:
6462:
6440:
6418:
6396:
6374:
6330:
6308:
6286:
6248:
6226:
6204:
6035:
6013:
5991:
5957:
5935:
5904:
5876:
5848:
5826:
5804:
5782:
5760:
5738:
5680:
5651:
5623:
5589:
5540:
5464:
5391:
5316:
5294:
5269:
5247:
5225:
5203:
5172:
5150:
5128:
5095:
5028:
5006:
4984:
4948:
4926:
4892:
4870:
4797:
4769:
4733:
4699:
4677:
4655:
4633:
4611:
4535:
4498:
4461:
4430:
4396:
4374:
4334:
4297:
4224:
4159:
4119:
4092:
4055:
4024:
3984:
3947:
3886:
3864:
3837:has value 1, and therefore is not valid.
3825:
3803:
3730:
3699:
3677:
3640:
3618:
3596:
3559:
3537:
3515:
3493:
3456:
3434:
3412:
3384:
3362:
3340:
3305:
3283:
3261:
3239:
3229:is true now or it is possible to perform
3217:
3195:
3173:
3145:
3123:
3101:
3079:
3057:
3035:
3011:
2983:
2939:
2855:
2786:
2721:
2652:
2613:
2576:
2516:
2482:
2460:
2438:
2416:
2394:
2372:
2344:
2288:
2266:
2244:
2222:
2200:
2178:
2154:
2132:
2110:
2088:
2066:
2044:
2020:
1984:
1962:
1934:
1853:
1784:
1719:
1650:
1611:
1578:
1518:
1435:
1371:
1336:
1310:
1288:
1262:
1235:
1213:
1187:
1155:
1133:
1111:
1081:
1049:
1021:
999:
966:
944:
922:
870:
814:
792:
770:
748:
726:
695:
673:
651:
629:
607:
572:
544:
516:
494:
449:
10269:Mirkowska, Grażyna; Salwicki A. (1987).
10237:
10213:Nicolas Troquard and Philippe Balbiani,
4302:{\displaystyle (b\to b)\to (b\to b)\,\!}
3845:As for modal logic, the inference rules
1939:{\displaystyle p\land (p\to p)\to p\,\!}
213:(doing one action followed by another),
8402:. Tests can be axiomatized as follows.
7732:is the superscript in the expansion of
7202:{\displaystyle \forall i\Phi (n+i)\,\!}
4229:{\displaystyle b\to b\vdash b\to b\,\!}
3952:{\displaystyle b\to b\vdash b\to b\,\!}
10360:
9080:{\displaystyle x\mathbin {:=} {?}\,\!}
8485:{\displaystyle \langle p?\rangle \,\!}
6558:; if it denotes 3 before incrementing
3876:for the action of kicking the TV, and
2963:changes nothing, bearing in mind that
2406:it remains the case that the truth of
2256:must bring about a situation in which
1789:{\displaystyle p\leftrightarrow p\,\!}
1655:{\displaystyle p\leftrightarrow p\,\!}
731:{\displaystyle \langle a\rangle p\,\!}
8919:zero or more times and then performs
7107:modalities. Then apply Hoare's axiom
5140:can be instantiated with any formula
4802:{\displaystyle \langle a\rangle \,\!}
3016:{\displaystyle \langle 1\rangle \,\!}
577:{\displaystyle \langle a\rangle \,\!}
372:{\displaystyle \varphi \to \varphi '}
8912:{\displaystyle p?\mathbin {;} a\,\!}
8662:{\displaystyle p?\mathbin {;} a\,\!}
6857:, that is, the conjunction over all
6408:as before, even though incrementing
3711:is false, or in any situation where
3689:will be true in any situation where
3571:will be true there. The implication
1192:{\displaystyle a{\mathbin {;}}b\,\!}
1123:, is performed by performing one of
10218:Stanford encyclopedia of philosophy
9051:Quantification as random assignment
7078:{\displaystyle \ldots \Phi (n)\,\!}
5109:This is a schema in the sense that
1383:, does nothing but does terminate.
1203:, is performed by performing first
18:dynamic logic (digital electronics)
13:
10195:
9387:
9324:
9026:
8976:
8926:
8865:
8698:
8582:
8012:
8006:
7973:
7952:
7943:
7928:
7869:
7692:
7658:
7652:
7625:
7610:
7601:
7586:
7491:
7485:
7452:
7431:
7422:
7407:
7367:
7361:
7334:
7292:
7283:
7268:
7179:
7173:
7136:
7061:
6985:
6920:
6827:
6778:
6729:
6664:
6274:
6192:
6141:
6105:
6057:
5923:
5288:
5266:
5222:
5191:
5147:
5116:
5083:
5068:
4236:is sound. However the implication
3808:{\displaystyle (x=1)\to (x=1)\,\!}
2915:
2598:
2570:
2558:
1429:
1417:
963:
941:
916:
904:
864:
852:
170:{\displaystyle \langle a\rangle p}
43:capable of encoding properties of
14:
10389:
10342:Chapter 6 : Logic and Action
10338:(original paper on dynamic logic)
10329:
10262:
9891:nondeterministic exponential time
9565:Propositional dynamic logic (PDL)
7682:, namely mathematical induction.
5635:, which in turn is equivalent to
2506:generalized to arbitrary actions
9930:by expressing the Hoare formula
9235:says that it is possible to set
9055:The random-assignment statement
8549:is realized in dynamic logic as
4960:might be greater or equal to 4.
3815:is false in any situation where
3207:sufficiently often, then either
641:it is necessarily the case that
619:is that after performing action
9922:Dynamic logic was developed by
206:{\displaystyle a\mathbin {;} b}
10352:Lecture Notes on Dynamic Logic
10231:
10215:"Propositional Dynamic Logic."
10137:sequential case. In contrast
10109:
10097:
10066:
10060:
10038:
10026:
9983:
9977:
9974:
9895:deterministic exponential time
9802:
9790:
9787:
9769:
9613:
9601:
9598:
9580:
9526:
9508:
9500:
9486:
9302:
9286:
9132:
9116:
8853:
8835:
8599:
8579:
8573:
8556:
8519:
8461:The corresponding theorem for
8444:
8438:
8432:
8429:
8423:
8414:
8223:
8214:
8211:
8208:
8202:
8196:
8193:
8187:
8184:
8175:
8027:
8015:
8003:
8000:
7997:
7994:
7976:
7970:
7967:
7955:
7949:
7937:
7931:
7925:
7878:
7872:
7667:
7661:
7649:
7646:
7643:
7640:
7628:
7622:
7619:
7613:
7607:
7595:
7589:
7583:
7506:
7494:
7482:
7479:
7476:
7473:
7455:
7449:
7446:
7434:
7428:
7416:
7410:
7404:
7382:
7370:
7358:
7355:
7352:
7349:
7337:
7331:
7313:
7310:
7307:
7295:
7289:
7277:
7271:
7265:
7243:
7237:
7219:
7216:
7194:
7182:
7159:{\displaystyle \Phi (n+i)\,\!}
7151:
7139:
7070:
7064:
7055:
7037:
7034:
7016:
6994:
6988:
6982:
6973:
6954:
6951:
6929:
6923:
6917:
6908:
6889:
6886:
6836:
6830:
6824:
6815:
6796:
6793:
6787:
6781:
6775:
6766:
6747:
6744:
6738:
6732:
6726:
6717:
6698:
6695:
6673:
6667:
6661:
6655:
6637:
6634:
6543:
6525:
6371:
6353:
6283:
6277:
6201:
6195:
6189:
6183:
6165:
6162:
6159:
6156:
6153:
6150:
6144:
6138:
6120:
6117:
6114:
6108:
6102:
6099:
6093:
6075:
6072:
6066:
6060:
6054:
5932:
5926:
5720:
5702:
5577:
5559:
5522:
5519:
5507:
5504:
5486:
5446:
5443:
5425:
5422:
5410:
5372:
5369:
5350:
5347:
5335:
5200:
5194:
5125:
5119:
5092:
5086:
5080:
5077:
5071:
5065:
5053:
4867:
4855:
4831:
4828:
4816:
4766:
4760:
4753:have the same force, that is,
4608:
4596:
4593:
4575:
4572:
4569:
4557:
4529:
4523:
4520:
4492:
4486:
4483:
4455:
4449:
4424:
4415:
4368:
4359:
4356:
4328:
4322:
4319:
4294:
4288:
4279:
4276:
4270:
4267:
4264:
4258:
4252:
4249:
4243:
4218:
4209:
4206:
4194:
4188:
4185:
4153:
4144:
4141:
4086:
4080:
4077:
4049:
4043:
4018:
4009:
4006:
3978:
3972:
3969:
3941:
3932:
3929:
3917:
3911:
3908:
3800:
3788:
3785:
3767:
3764:
3761:
3749:
3724:
3718:
3671:
3665:
3662:
3590:
3584:
3581:
3487:
3481:
3334:
3025:T3 says that if the choice of
2980:
2974:
2936:
2912:
2891:
2822:
2762:
2691:
2646:
2555:
2549:
2543:
2531:
1928:
1919:
1916:
1913:
1907:
1901:
1898:
1892:
1889:
1880:
1847:
1838:
1835:
1829:
1820:
1814:
1805:
1778:
1772:
1769:
1763:
1760:
1754:
1740:
1713:
1707:
1698:
1692:
1689:
1683:
1671:
1644:
1638:
1632:
1605:
1599:
1572:
1566:
1489:
1414:
1408:
1402:
1104:
913:
907:
901:
849:
843:
837:
601:
595:
541:
535:
358:
352:
349:
339:, the dynamic logic statement
124:
118:
76:
68:
65:
1:
10296:
9810:{\displaystyle (x\geq 4)\,\!}
9621:{\displaystyle (x\geq 4)\,\!}
9398:{\displaystyle \exists x\,\!}
9335:{\displaystyle \forall x\,\!}
9172:holds no matter what you set
7703:{\displaystyle \forall i\,\!}
6346:with respect to the modality
5628:{\displaystyle x+1\geq 4\,\!}
5299:{\displaystyle \forall x\,\!}
4963:
3498:{\displaystyle p\vdash p\,\!}
3417:{\displaystyle p\vdash q\,\!}
2034:A3 says that if doing one of
1498:{\displaystyle \vdash p\to q}
1278:, is performed by performing
461:is necessarily the case, and
10224:
10084:corresponding to Dijkstra's
8727:is equivalent to BLOCK, and
7886:{\displaystyle \Phi (n)\,\!}
7002:{\displaystyle \Phi (n)\,\!}
6937:{\displaystyle \Phi (n)\,\!}
6688:as the infinite conjunction
6681:{\displaystyle \Phi (n)\,\!}
6291:{\displaystyle \Phi (n)\,\!}
5940:{\displaystyle \Phi (n)\,\!}
5772:sufficiently often, to make
5208:{\displaystyle \Phi (e)\,\!}
5133:{\displaystyle \Phi (x)\,\!}
1447:and the two inference rules
971:{\displaystyle \exists \,\!}
949:{\displaystyle \forall \,\!}
33:theoretical computer science
7:
10241:A Discipline of Programming
10156:
9957:{\displaystyle p\{a\}q\,\!}
9755:{\displaystyle x\geq 4\,\!}
9040:{\displaystyle \neg p?\,\!}
8990:{\displaystyle \neg p?\,\!}
8940:{\displaystyle \neg p?\,\!}
8748:{\displaystyle a\cup 0\,\!}
6474:, even though incrementing
5881:{\displaystyle x\leq 7\,\!}
5656:{\displaystyle x\geq 3\,\!}
5594:{\displaystyle x\geq 4\,\!}
3742:is true, but the assertion
1054:{\displaystyle a\cup b\,\!}
484:(diamond p) asserting that
405:
10:
10394:
9994:{\displaystyle p\to q\,\!}
9917:
9910:(1978), Pratt (1979), and
9875:{\displaystyle x:=x+1\,\!}
9727:{\displaystyle x:=x+1\,\!}
9628:contains all three types:
5996:{\displaystyle n:=n+1\,\!}
5237:with those occurrences of
4931:{\displaystyle x:=x+1\,\!}
4738:{\displaystyle x:=x+1\,\!}
4540:{\displaystyle b\to b\,\!}
4503:{\displaystyle b\to b\,\!}
4379:{\displaystyle b\to b\,\!}
4339:{\displaystyle b\to b\,\!}
4164:{\displaystyle b\to b\,\!}
4097:{\displaystyle b\to b\,\!}
4029:{\displaystyle b\to b\,\!}
3989:{\displaystyle b\to b\,\!}
3841:Derived rules of inference
3682:{\displaystyle p\to p\,\!}
3601:{\displaystyle p\to p\,\!}
3345:{\displaystyle p\to q\,\!}
3161:T5 is explained as for A5.
1582:{\displaystyle \vdash p\,}
1522:{\displaystyle \vdash q\,}
477:{\displaystyle \Diamond p}
15:
10373:Logic in computer science
10184:Temporal logic of actions
10132:The concurrency challenge
9561:including dynamic logic.
7788:over all natural numbers
7781:{\displaystyle a^{i}\,\!}
7129:times to this to produce
5274:{\displaystyle \Phi \,\!}
5230:{\displaystyle \Phi \,\!}
5155:{\displaystyle \Phi \,\!}
1386:
738:is that after performing
332:{\displaystyle \varphi '}
9887:computational complexity
9548:Possible-world semantics
9426:{\displaystyle x:=?\,\!}
7752:{\displaystyle a{*}\,\!}
4989:{\displaystyle x:=e\,\!}
4124:{\displaystyle k{*}\,\!}
3135:alone could bring about
2494:. A6 is recognizable as
1549:{\displaystyle \vdash p}
1469:{\displaystyle \vdash p}
1376:{\displaystyle 0{*}\,\!}
1267:{\displaystyle a{*}\,\!}
413:is characterized by the
304:{\displaystyle \varphi }
10238:Dijkstra, E.W. (1976).
9823:propositional variables
9671:{\displaystyle x+1\,\!}
9109:to an arbitrary value.
8248:
8133:{\displaystyle n+i\,\!}
8064:in that state, as when
7862:is a real variable and
7568:in the usual manner of
6944:. Now apply A4 to turn
1167:. The compound action
1116:{\displaystyle a|b\,\!}
1086:{\displaystyle a+b\,\!}
439:(box p) asserting that
232:{\displaystyle a\cup b}
10126:predicate transformers
10118:
10078:
10047:
9995:
9958:
9876:
9811:
9756:
9728:
9694:
9672:
9644:
9622:
9538:
9473:
9453:
9427:
9399:
9374:
9336:
9311:
9273:
9257:to a value that makes
9251:
9229:
9188:
9166:
9144:
9103:
9081:
9041:
9013:
8991:
8963:
8941:
8913:
8880:
8815:
8793:
8771:
8749:
8721:
8685:
8663:
8630:
8608:
8537:
8486:
8453:
8392:
8391:{\displaystyle p?\,\!}
8367:
8341:
8340:{\displaystyle p?\,\!}
8316:
8294:
8293:{\displaystyle p?\,\!}
8269:
8235:
8156:
8134:
8106:
8090:. If in a given state
8080:
8058:
8036:
7909:
7887:
7856:
7826:
7804:
7782:
7753:
7726:
7704:
7676:
7562:
7540:
7515:
7391:
7252:
7203:
7160:
7123:
7101:
7079:
7003:
6938:
6873:
6851:
6682:
6618:
6596:
6574:
6552:
6512:
6490:
6468:
6446:
6424:
6402:
6380:
6336:
6314:
6292:
6254:
6232:
6210:
6041:
6019:
5997:
5963:
5941:
5910:
5892:Mathematical induction
5882:
5854:
5832:
5810:
5788:
5766:
5744:
5686:
5657:
5629:
5595:
5546:
5470:
5397:
5322:
5300:
5275:
5253:
5231:
5209:
5178:
5156:
5134:
5101:
5034:
5012:
4990:
4954:
4932:
4898:
4876:
4803:
4775:
4739:
4705:
4683:
4661:
4639:
4617:
4541:
4504:
4467:
4436:
4402:
4380:
4340:
4303:
4230:
4165:
4125:
4098:
4061:
4030:
3990:
3953:
3892:
3870:
3831:
3809:
3736:
3705:
3683:
3646:
3624:
3602:
3565:
3543:
3521:
3499:
3462:
3440:
3418:
3390:
3368:
3346:
3311:
3289:
3267:
3245:
3223:
3201:
3179:
3151:
3129:
3107:
3085:
3063:
3041:
3017:
2989:
2945:
2861:
2792:
2727:
2658:
2619:
2582:
2536:The modal logic axiom
2522:
2496:mathematical induction
2488:
2466:
2444:
2422:
2400:
2378:
2350:
2294:
2272:
2250:
2228:
2206:
2184:
2168:A4 says that if doing
2160:
2138:
2116:
2094:
2072:
2050:
2026:
1990:
1968:
1940:
1859:
1790:
1725:
1656:
1617:
1583:
1550:
1523:
1499:
1470:
1441:
1377:
1342:
1316:
1294:
1268:
1247:. The compound action
1241:
1219:
1193:
1161:
1139:
1117:
1087:
1055:
1033:, the compound action
1027:
1005:
972:
950:
928:
876:
820:
798:
776:
754:
732:
701:
679:
657:
635:
613:
584:, thereby making it a
578:
550:
522:
500:
478:
455:
433:
432:{\displaystyle \Box p}
373:
333:
305:
282:
258:
233:
207:
171:
134:
91:
10119:
10079:
10077:{\displaystyle p\,\!}
10048:
9996:
9959:
9877:
9812:
9757:
9729:
9695:
9693:{\displaystyle 4\,\!}
9673:
9645:
9643:{\displaystyle x\,\!}
9623:
9539:
9474:
9454:
9428:
9400:
9375:
9337:
9312:
9274:
9272:{\displaystyle p\,\!}
9252:
9250:{\displaystyle x\,\!}
9230:
9189:
9187:{\displaystyle x\,\!}
9167:
9165:{\displaystyle p\,\!}
9145:
9143:{\displaystyle p\,\!}
9104:
9102:{\displaystyle x\,\!}
9082:
9042:
9014:
9012:{\displaystyle p\,\!}
8992:
8964:
8962:{\displaystyle p\,\!}
8942:
8914:
8881:
8816:
8814:{\displaystyle p\,\!}
8794:
8792:{\displaystyle p\,\!}
8772:
8770:{\displaystyle a\,\!}
8750:
8722:
8686:
8684:{\displaystyle a\,\!}
8664:
8631:
8629:{\displaystyle p\,\!}
8609:
8538:
8487:
8454:
8393:
8368:
8366:{\displaystyle p\,\!}
8342:
8317:
8315:{\displaystyle p\,\!}
8295:
8270:
8268:{\displaystyle p\,\!}
8236:
8157:
8155:{\displaystyle n\,\!}
8135:
8107:
8105:{\displaystyle n\,\!}
8081:
8079:{\displaystyle n\,\!}
8059:
8057:{\displaystyle n\,\!}
8037:
7910:
7908:{\displaystyle n\,\!}
7888:
7857:
7855:{\displaystyle n\,\!}
7827:
7825:{\displaystyle n\,\!}
7805:
7803:{\displaystyle i\,\!}
7783:
7754:
7727:
7725:{\displaystyle i\,\!}
7705:
7677:
7563:
7561:{\displaystyle n\,\!}
7541:
7539:{\displaystyle 0\,\!}
7516:
7392:
7253:
7204:
7161:
7124:
7122:{\displaystyle i\,\!}
7102:
7100:{\displaystyle i\,\!}
7080:
7004:
6939:
6874:
6872:{\displaystyle i\,\!}
6852:
6683:
6619:
6617:{\displaystyle n\,\!}
6597:
6595:{\displaystyle 0\,\!}
6575:
6573:{\displaystyle n\,\!}
6553:
6513:
6511:{\displaystyle n\,\!}
6491:
6489:{\displaystyle n\,\!}
6469:
6467:{\displaystyle n\,\!}
6447:
6445:{\displaystyle a\,\!}
6425:
6423:{\displaystyle n\,\!}
6403:
6401:{\displaystyle n\,\!}
6381:
6337:
6335:{\displaystyle p\,\!}
6315:
6313:{\displaystyle p\,\!}
6293:
6255:
6253:{\displaystyle n\,\!}
6233:
6231:{\displaystyle 0\,\!}
6211:
6042:
6040:{\displaystyle 0\,\!}
6020:
6018:{\displaystyle n\,\!}
5998:
5964:
5962:{\displaystyle a\,\!}
5942:
5911:
5909:{\displaystyle p\,\!}
5883:
5855:
5853:{\displaystyle x\,\!}
5833:
5831:{\displaystyle x\,\!}
5811:
5809:{\displaystyle x\,\!}
5789:
5787:{\displaystyle x\,\!}
5767:
5765:{\displaystyle x\,\!}
5745:
5687:
5685:{\displaystyle *\,\!}
5658:
5630:
5596:
5547:
5471:
5398:
5323:
5321:{\displaystyle e\,\!}
5301:
5276:
5254:
5252:{\displaystyle x\,\!}
5232:
5210:
5179:
5177:{\displaystyle x\,\!}
5157:
5135:
5102:
5035:
5033:{\displaystyle e\,\!}
5013:
5011:{\displaystyle x\,\!}
4991:
4955:
4953:{\displaystyle x\,\!}
4933:
4899:
4897:{\displaystyle x\,\!}
4877:
4804:
4776:
4740:
4706:
4704:{\displaystyle a\,\!}
4684:
4682:{\displaystyle x\,\!}
4662:
4660:{\displaystyle x\,\!}
4640:
4638:{\displaystyle x\,\!}
4618:
4542:
4505:
4468:
4466:{\displaystyle b\,\!}
4442:must be false, while
4437:
4435:{\displaystyle b\,\!}
4403:
4401:{\displaystyle b\,\!}
4381:
4341:
4304:
4231:
4166:
4126:
4099:
4062:
4060:{\displaystyle b\,\!}
4031:
3991:
3954:
3893:
3891:{\displaystyle b\,\!}
3871:
3869:{\displaystyle k\,\!}
3832:
3830:{\displaystyle x\,\!}
3810:
3737:
3735:{\displaystyle p\,\!}
3706:
3704:{\displaystyle p\,\!}
3684:
3647:
3645:{\displaystyle a\,\!}
3625:
3623:{\displaystyle p\,\!}
3603:
3566:
3564:{\displaystyle p\,\!}
3544:
3542:{\displaystyle a\,\!}
3522:
3520:{\displaystyle p\,\!}
3500:
3463:
3461:{\displaystyle q\,\!}
3441:
3439:{\displaystyle p\,\!}
3419:
3391:
3389:{\displaystyle q\,\!}
3369:
3367:{\displaystyle p\,\!}
3347:
3312:
3310:{\displaystyle p\,\!}
3290:
3288:{\displaystyle a\,\!}
3268:
3266:{\displaystyle p\,\!}
3246:
3244:{\displaystyle a\,\!}
3224:
3222:{\displaystyle p\,\!}
3202:
3200:{\displaystyle a\,\!}
3180:
3178:{\displaystyle p\,\!}
3152:
3150:{\displaystyle p\,\!}
3130:
3128:{\displaystyle b\,\!}
3108:
3106:{\displaystyle a\,\!}
3086:
3084:{\displaystyle p\,\!}
3064:
3062:{\displaystyle b\,\!}
3042:
3040:{\displaystyle a\,\!}
3018:
2990:
2946:
2862:
2793:
2728:
2659:
2620:
2583:
2523:
2521:{\displaystyle a\,\!}
2489:
2487:{\displaystyle a\,\!}
2467:
2465:{\displaystyle p\,\!}
2445:
2443:{\displaystyle a\,\!}
2423:
2421:{\displaystyle p\,\!}
2401:
2399:{\displaystyle a\,\!}
2379:
2377:{\displaystyle p\,\!}
2351:
2295:
2293:{\displaystyle p\,\!}
2273:
2271:{\displaystyle b\,\!}
2251:
2249:{\displaystyle a\,\!}
2229:
2227:{\displaystyle p\,\!}
2207:
2205:{\displaystyle b\,\!}
2185:
2183:{\displaystyle a\,\!}
2161:
2159:{\displaystyle b\,\!}
2139:
2137:{\displaystyle p\,\!}
2117:
2115:{\displaystyle a\,\!}
2095:
2093:{\displaystyle p\,\!}
2073:
2071:{\displaystyle b\,\!}
2051:
2049:{\displaystyle a\,\!}
2027:
2025:{\displaystyle p\,\!}
1991:
1989:{\displaystyle p\,\!}
1969:
1967:{\displaystyle p\,\!}
1941:
1860:
1791:
1726:
1657:
1618:
1616:{\displaystyle p\,\!}
1584:
1551:
1524:
1500:
1471:
1442:
1378:
1343:
1341:{\displaystyle 1\,\!}
1317:
1315:{\displaystyle 0\,\!}
1295:
1293:{\displaystyle a\,\!}
1269:
1242:
1240:{\displaystyle b\,\!}
1220:
1218:{\displaystyle a\,\!}
1194:
1162:
1160:{\displaystyle b\,\!}
1140:
1138:{\displaystyle a\,\!}
1118:
1088:
1056:
1028:
1026:{\displaystyle b\,\!}
1006:
1004:{\displaystyle a\,\!}
973:
951:
929:
877:
821:
819:{\displaystyle p\,\!}
799:
797:{\displaystyle a\,\!}
777:
775:{\displaystyle p\,\!}
755:
753:{\displaystyle a\,\!}
733:
702:
700:{\displaystyle p\,\!}
680:
678:{\displaystyle a\,\!}
658:
656:{\displaystyle p\,\!}
636:
634:{\displaystyle a\,\!}
614:
612:{\displaystyle p\,\!}
579:
551:
523:
521:{\displaystyle a\,\!}
501:
499:{\displaystyle p\,\!}
479:
456:
454:{\displaystyle p\,\!}
434:
374:
334:
306:
283:
259:
234:
208:
172:
135:
92:
10088:
10057:
10017:
9968:
9934:
9906:(unpublished note),
9852:
9766:
9738:
9704:
9682:
9654:
9632:
9577:
9483:
9463:
9443:
9409:
9384:
9346:
9321:
9310:{\displaystyle \,\!}
9283:
9261:
9239:
9198:
9176:
9154:
9113:
9091:
9059:
9023:
9001:
8973:
8951:
8923:
8890:
8832:
8821:is false the right.
8803:
8781:
8759:
8731:
8695:
8673:
8640:
8618:
8553:
8501:
8465:
8411:
8377:
8355:
8326:
8304:
8300:called a test. When
8279:
8257:
8166:
8144:
8116:
8094:
8068:
8046:
7922:
7897:
7866:
7844:
7814:
7792:
7763:
7736:
7714:
7689:
7580:
7576:'s celebrated axiom
7550:
7528:
7401:
7262:
7251:{\displaystyle \,\!}
7213:
7170:
7133:
7111:
7089:
7013:
6948:
6883:
6861:
6692:
6631:
6606:
6584:
6562:
6551:{\displaystyle \,\!}
6522:
6500:
6478:
6456:
6434:
6412:
6390:
6379:{\displaystyle \,\!}
6350:
6324:
6302:
6271:
6267:When we substituted
6242:
6220:
6051:
6029:
6007:
5973:
5951:
5920:
5898:
5864:
5842:
5820:
5798:
5776:
5754:
5696:
5674:
5639:
5605:
5556:
5483:
5407:
5332:
5310:
5285:
5263:
5241:
5219:
5188:
5166:
5144:
5113:
5050:
5022:
5000:
4972:
4942:
4908:
4886:
4813:
4785:
4774:{\displaystyle \,\!}
4757:
4715:
4693:
4671:
4649:
4627:
4623:. This says that if
4554:
4514:
4477:
4446:
4412:
4390:
4350:
4313:
4240:
4179:
4135:
4108:
4071:
4040:
4000:
3963:
3959:, having as premise
3902:
3880:
3858:
3819:
3746:
3715:
3693:
3656:
3634:
3612:
3575:
3553:
3531:
3509:
3472:
3450:
3446:is valid then so is
3428:
3400:
3378:
3356:
3328:
3299:
3277:
3255:
3233:
3211:
3189:
3167:
3139:
3117:
3095:
3073:
3051:
3029:
3023:have the same force.
2999:
2988:{\displaystyle \,\!}
2971:
2959:T2 notes again that
2873:
2804:
2739:
2670:
2631:
2595:
2540:
2510:
2476:
2454:
2432:
2410:
2388:
2366:
2306:
2282:
2260:
2238:
2216:
2194:
2172:
2148:
2126:
2104:
2082:
2060:
2038:
2014:
1978:
1956:
1871:
1802:
1737:
1668:
1629:
1596:
1560:
1537:
1509:
1480:
1457:
1399:
1360:
1330:
1304:
1282:
1251:
1229:
1207:
1171:
1149:
1127:
1097:
1069:
1037:
1015:
993:
960:
938:
886:
834:
808:
786:
764:
760:it is possible that
742:
711:
689:
667:
645:
623:
592:
560:
549:{\displaystyle \,\!}
532:
528:the modal operators
510:
488:
465:
443:
420:
402:, and other fields.
343:
318:
295:
272:
257:{\displaystyle a{*}}
243:
217:
189:
181:it is possible that
152:
115:
57:
10378:Non-classical logic
9914:and Parikh (1981).
9819:Propositional logic
7916:is a natural number
6262:referential opacity
5916:is instantiated as
5692:is the proposition
5259:that occur free in
3374:is true then so is
3159:T4 is just like A4.
2362:A6 asserts that if
1996:is the proposition
1974:will hold, even if
956:) and existential (
826:. These operators
388:formal verification
39:is an extension of
10141:'s 1977 system of
10114:
10074:
10043:
9991:
9954:
9872:
9842:Michael J. Fischer
9807:
9752:
9734:is an action, and
9724:
9690:
9668:
9640:
9618:
9534:
9469:
9449:
9423:
9395:
9370:
9332:
9307:
9269:
9247:
9225:
9184:
9162:
9140:
9099:
9077:
9037:
9009:
8987:
8969:remains true, the
8959:
8937:
8909:
8876:
8811:
8789:
8767:
8745:
8717:
8681:
8659:
8626:
8604:
8547:if p then a else b
8533:
8482:
8449:
8388:
8363:
8337:
8312:
8290:
8265:
8231:
8152:
8130:
8102:
8076:
8054:
8032:
7905:
7883:
7852:
7822:
7800:
7778:
7749:
7722:
7700:
7672:
7558:
7536:
7511:
7387:
7248:
7199:
7156:
7119:
7097:
7075:
6999:
6934:
6869:
6847:
6678:
6624:everywhere in A6.
6614:
6592:
6570:
6548:
6508:
6486:
6464:
6442:
6420:
6398:
6376:
6332:
6310:
6288:
6250:
6228:
6206:
6037:
6015:
5993:
5959:
5937:
5906:
5878:
5850:
5828:
5806:
5784:
5762:
5740:
5682:
5665:elementary algebra
5653:
5625:
5591:
5542:
5466:
5393:
5318:
5296:
5271:
5249:
5227:
5205:
5174:
5152:
5130:
5097:
5030:
5018:is a variable and
5008:
4986:
4950:
4928:
4894:
4882:asserting that if
4872:
4799:
4771:
4735:
4701:
4679:
4657:
4635:
4613:
4537:
4500:
4463:
4432:
4398:
4376:
4336:
4299:
4226:
4161:
4121:
4094:
4057:
4026:
3996:and as conclusion
3986:
3949:
3888:
3866:
3827:
3805:
3732:
3701:
3679:
3642:
3620:
3598:
3561:
3539:
3517:
3495:
3458:
3436:
3414:
3386:
3364:
3342:
3307:
3295:could bring about
3285:
3263:
3241:
3219:
3197:
3175:
3147:
3125:
3103:
3081:
3069:could bring about
3059:
3037:
3013:
2985:
2941:
2857:
2788:
2723:
2654:
2615:
2578:
2518:
2484:
2462:
2440:
2418:
2396:
2374:
2346:
2290:
2268:
2246:
2224:
2202:
2180:
2156:
2134:
2112:
2090:
2068:
2046:
2022:
1986:
1964:
1936:
1855:
1786:
1721:
1652:
1613:
1579:
1546:
1519:
1495:
1466:
1437:
1373:
1338:
1312:
1290:
1264:
1237:
1215:
1189:
1157:
1135:
1113:
1083:
1051:
1023:
1001:
987:regular expression
968:
946:
924:
872:
816:
804:might bring about
794:
772:
750:
728:
707:. The meaning of
697:
675:
653:
631:
609:
588:. The meaning of
574:
546:
518:
496:
474:
451:
429:
386:Beyond its use in
369:
329:
301:
278:
266:Boolean operations
254:
229:
203:
167:
130:
87:
10272:Algorithmic Logic
10153:, fairness, etc.
10007:algorithmic logic
9571:first-order logic
9472:{\displaystyle x}
9452:{\displaystyle x}
8755:is equivalent to
8669:is equivalent to
7893:is the predicate
7832:had been of type
7570:first-order logic
5184:. The meaning of
4036:. The meaning of
2278:must bring about
2212:must bring about
2166:, and conversely.
2144:and likewise for
2122:must bring about
2078:must bring about
685:must bring about
281:{\displaystyle P}
148:should hold, and
133:{\displaystyle p}
82:
81:The ground is wet
74:
63:
62:The ground is dry
45:computer programs
10385:
10354:by André Platzer
10309:, 1976, 109-121.
10290:
10289:
10277:
10266:
10260:
10259:
10235:
10189:Modal μ-calculus
10123:
10121:
10120:
10115:
10083:
10081:
10080:
10075:
10052:
10050:
10049:
10044:
10000:
9998:
9997:
9992:
9963:
9961:
9960:
9955:
9881:
9879:
9878:
9873:
9817:are assertions.
9816:
9814:
9813:
9808:
9761:
9759:
9758:
9753:
9733:
9731:
9730:
9725:
9699:
9697:
9696:
9691:
9677:
9675:
9674:
9669:
9649:
9647:
9646:
9641:
9627:
9625:
9624:
9619:
9559:systems of logic
9543:
9541:
9540:
9535:
9533:
9507:
9496:
9478:
9476:
9475:
9470:
9458:
9456:
9455:
9450:
9432:
9430:
9429:
9424:
9404:
9402:
9401:
9396:
9379:
9377:
9376:
9371:
9364:
9359:
9341:
9339:
9338:
9333:
9316:
9314:
9313:
9308:
9301:
9296:
9278:
9276:
9275:
9270:
9256:
9254:
9253:
9248:
9234:
9232:
9231:
9226:
9216:
9211:
9193:
9191:
9190:
9185:
9171:
9169:
9168:
9163:
9149:
9147:
9146:
9141:
9131:
9126:
9108:
9106:
9105:
9100:
9086:
9084:
9083:
9078:
9074:
9069:
9046:
9044:
9043:
9038:
9018:
9016:
9015:
9010:
8996:
8994:
8993:
8988:
8968:
8966:
8965:
8960:
8946:
8944:
8943:
8938:
8918:
8916:
8915:
8910:
8903:
8886:. This performs
8885:
8883:
8882:
8877:
8864:
8859:
8849:
8820:
8818:
8817:
8812:
8798:
8796:
8795:
8790:
8776:
8774:
8773:
8768:
8754:
8752:
8751:
8746:
8726:
8724:
8723:
8718:
8711:
8690:
8688:
8687:
8682:
8668:
8666:
8665:
8660:
8653:
8635:
8633:
8632:
8627:
8613:
8611:
8610:
8605:
8595:
8569:
8542:
8540:
8539:
8534:
8491:
8489:
8488:
8483:
8458:
8456:
8455:
8450:
8397:
8395:
8394:
8389:
8372:
8370:
8369:
8364:
8346:
8344:
8343:
8338:
8322:holds, the test
8321:
8319:
8318:
8313:
8299:
8297:
8296:
8291:
8274:
8272:
8271:
8266:
8240:
8238:
8237:
8232:
8161:
8159:
8158:
8153:
8139:
8137:
8136:
8131:
8111:
8109:
8108:
8103:
8085:
8083:
8082:
8077:
8063:
8061:
8060:
8055:
8041:
8039:
8038:
8033:
7914:
7912:
7911:
7906:
7892:
7890:
7889:
7884:
7861:
7859:
7858:
7853:
7831:
7829:
7828:
7823:
7809:
7807:
7806:
7801:
7787:
7785:
7784:
7779:
7775:
7774:
7759:as the union of
7758:
7756:
7755:
7750:
7746:
7731:
7729:
7728:
7723:
7709:
7707:
7706:
7701:
7681:
7679:
7678:
7673:
7567:
7565:
7564:
7559:
7545:
7543:
7542:
7537:
7520:
7518:
7517:
7512:
7396:
7394:
7393:
7388:
7258:in A6, yielding
7257:
7255:
7254:
7249:
7208:
7206:
7205:
7200:
7165:
7163:
7162:
7157:
7128:
7126:
7125:
7120:
7106:
7104:
7103:
7098:
7084:
7082:
7081:
7076:
7008:
7006:
7005:
7000:
6981:
6980:
6943:
6941:
6940:
6935:
6916:
6915:
6878:
6876:
6875:
6870:
6856:
6854:
6853:
6848:
6823:
6822:
6774:
6773:
6725:
6724:
6687:
6685:
6684:
6679:
6623:
6621:
6620:
6615:
6601:
6599:
6598:
6593:
6579:
6577:
6576:
6571:
6557:
6555:
6554:
6549:
6517:
6515:
6514:
6509:
6495:
6493:
6492:
6487:
6473:
6471:
6470:
6465:
6451:
6449:
6448:
6443:
6429:
6427:
6426:
6421:
6407:
6405:
6404:
6399:
6385:
6383:
6382:
6377:
6344:rigid designator
6341:
6339:
6338:
6333:
6319:
6317:
6316:
6311:
6297:
6295:
6294:
6289:
6259:
6257:
6256:
6251:
6237:
6235:
6234:
6229:
6215:
6213:
6212:
6207:
6046:
6044:
6043:
6038:
6024:
6022:
6021:
6016:
6002:
6000:
5999:
5994:
5968:
5966:
5965:
5960:
5946:
5944:
5943:
5938:
5915:
5913:
5912:
5907:
5887:
5885:
5884:
5879:
5859:
5857:
5856:
5851:
5837:
5835:
5834:
5829:
5815:
5813:
5812:
5807:
5793:
5791:
5790:
5785:
5771:
5769:
5768:
5763:
5749:
5747:
5746:
5741:
5691:
5689:
5688:
5683:
5662:
5660:
5659:
5654:
5634:
5632:
5631:
5626:
5600:
5598:
5597:
5592:
5551:
5549:
5548:
5543:
5475:
5473:
5472:
5467:
5402:
5400:
5399:
5394:
5390:
5389:
5368:
5367:
5327:
5325:
5324:
5319:
5305:
5303:
5302:
5297:
5280:
5278:
5277:
5272:
5258:
5256:
5255:
5250:
5236:
5234:
5233:
5228:
5214:
5212:
5211:
5206:
5183:
5181:
5180:
5175:
5161:
5159:
5158:
5153:
5139:
5137:
5136:
5131:
5106:
5104:
5103:
5098:
5039:
5037:
5036:
5031:
5017:
5015:
5014:
5009:
4995:
4993:
4992:
4987:
4959:
4957:
4956:
4951:
4937:
4935:
4934:
4929:
4903:
4901:
4900:
4895:
4881:
4879:
4878:
4873:
4808:
4806:
4805:
4800:
4780:
4778:
4777:
4772:
4744:
4742:
4741:
4736:
4710:
4708:
4707:
4702:
4688:
4686:
4685:
4680:
4666:
4664:
4663:
4658:
4644:
4642:
4641:
4636:
4622:
4620:
4619:
4614:
4546:
4544:
4543:
4538:
4509:
4507:
4506:
4501:
4472:
4470:
4469:
4464:
4441:
4439:
4438:
4433:
4407:
4405:
4404:
4399:
4385:
4383:
4382:
4377:
4345:
4343:
4342:
4337:
4308:
4306:
4305:
4300:
4235:
4233:
4232:
4227:
4170:
4168:
4167:
4162:
4130:
4128:
4127:
4122:
4118:
4103:
4101:
4100:
4095:
4066:
4064:
4063:
4058:
4035:
4033:
4032:
4027:
3995:
3993:
3992:
3987:
3958:
3956:
3955:
3950:
3897:
3895:
3894:
3889:
3875:
3873:
3872:
3867:
3836:
3834:
3833:
3828:
3814:
3812:
3811:
3806:
3741:
3739:
3738:
3733:
3710:
3708:
3707:
3702:
3688:
3686:
3685:
3680:
3651:
3649:
3648:
3643:
3629:
3627:
3626:
3621:
3607:
3605:
3604:
3599:
3570:
3568:
3567:
3562:
3548:
3546:
3545:
3540:
3526:
3524:
3523:
3518:
3504:
3502:
3501:
3496:
3467:
3465:
3464:
3459:
3445:
3443:
3442:
3437:
3424:asserts that if
3423:
3421:
3420:
3415:
3396:, the inference
3395:
3393:
3392:
3387:
3373:
3371:
3370:
3365:
3352:asserts that if
3351:
3349:
3348:
3343:
3316:
3314:
3313:
3308:
3294:
3292:
3291:
3286:
3272:
3270:
3269:
3264:
3250:
3248:
3247:
3242:
3228:
3226:
3225:
3220:
3206:
3204:
3203:
3198:
3184:
3182:
3181:
3176:
3156:
3154:
3153:
3148:
3134:
3132:
3131:
3126:
3112:
3110:
3109:
3104:
3090:
3088:
3087:
3082:
3068:
3066:
3065:
3060:
3046:
3044:
3043:
3038:
3022:
3020:
3019:
3014:
2994:
2992:
2991:
2986:
2950:
2948:
2947:
2942:
2866:
2864:
2863:
2858:
2797:
2795:
2794:
2789:
2752:
2732:
2730:
2729:
2724:
2663:
2661:
2660:
2655:
2624:
2622:
2621:
2616:
2587:
2585:
2584:
2579:
2527:
2525:
2524:
2519:
2502:of incrementing
2498:with the action
2493:
2491:
2490:
2485:
2471:
2469:
2468:
2463:
2449:
2447:
2446:
2441:
2427:
2425:
2424:
2419:
2405:
2403:
2402:
2397:
2383:
2381:
2380:
2375:
2355:
2353:
2352:
2347:
2343:
2335:
2334:
2316:
2299:
2297:
2296:
2291:
2277:
2275:
2274:
2269:
2255:
2253:
2252:
2247:
2233:
2231:
2230:
2225:
2211:
2209:
2208:
2203:
2189:
2187:
2186:
2181:
2165:
2163:
2162:
2157:
2143:
2141:
2140:
2135:
2121:
2119:
2118:
2113:
2099:
2097:
2096:
2091:
2077:
2075:
2074:
2069:
2055:
2053:
2052:
2047:
2031:
2029:
2028:
2023:
1995:
1993:
1992:
1987:
1973:
1971:
1970:
1965:
1945:
1943:
1942:
1937:
1864:
1862:
1861:
1856:
1795:
1793:
1792:
1787:
1750:
1730:
1728:
1727:
1722:
1661:
1659:
1658:
1653:
1622:
1620:
1619:
1614:
1588:
1586:
1585:
1580:
1555:
1553:
1552:
1547:
1528:
1526:
1525:
1520:
1504:
1502:
1501:
1496:
1475:
1473:
1472:
1467:
1446:
1444:
1443:
1438:
1382:
1380:
1379:
1374:
1370:
1347:
1345:
1344:
1339:
1321:
1319:
1318:
1313:
1299:
1297:
1296:
1291:
1273:
1271:
1270:
1265:
1261:
1246:
1244:
1243:
1238:
1224:
1222:
1221:
1216:
1198:
1196:
1195:
1190:
1183:
1182:
1166:
1164:
1163:
1158:
1144:
1142:
1141:
1136:
1122:
1120:
1119:
1114:
1107:
1092:
1090:
1089:
1084:
1060:
1058:
1057:
1052:
1032:
1030:
1029:
1024:
1010:
1008:
1007:
1002:
977:
975:
974:
969:
955:
953:
952:
947:
933:
931:
930:
925:
881:
879:
878:
873:
825:
823:
822:
817:
803:
801:
800:
795:
782:holds, that is,
781:
779:
778:
773:
759:
757:
756:
751:
737:
735:
734:
729:
706:
704:
703:
698:
684:
682:
681:
676:
663:holds, that is,
662:
660:
659:
654:
640:
638:
637:
632:
618:
616:
615:
610:
586:multimodal logic
583:
581:
580:
575:
555:
553:
552:
547:
527:
525:
524:
519:
505:
503:
502:
497:
483:
481:
480:
475:
460:
458:
457:
452:
438:
436:
435:
430:
378:
376:
375:
370:
368:
338:
336:
335:
330:
328:
310:
308:
307:
302:
287:
285:
284:
279:
263:
261:
260:
255:
253:
238:
236:
235:
230:
212:
210:
209:
204:
199:
176:
174:
173:
168:
144:the proposition
139:
137:
136:
131:
96:
94:
93:
88:
83:
80:
75:
72:
64:
61:
10393:
10392:
10388:
10387:
10386:
10384:
10383:
10382:
10358:
10357:
10346:Logic In Action
10332:
10299:
10294:
10293:
10286:
10275:
10267:
10263:
10256:
10236:
10232:
10227:
10198:
10196:Further reading
10193:
10159:
10134:
10089:
10086:
10085:
10058:
10055:
10054:
10018:
10015:
10014:
10011:Edsger Dijkstra
9969:
9966:
9965:
9935:
9932:
9931:
9920:
9893:, and at least
9853:
9850:
9849:
9767:
9764:
9763:
9739:
9736:
9735:
9705:
9702:
9701:
9683:
9680:
9679:
9655:
9652:
9651:
9633:
9630:
9629:
9578:
9575:
9574:
9567:
9550:
9529:
9503:
9492:
9484:
9481:
9480:
9464:
9461:
9460:
9444:
9441:
9440:
9410:
9407:
9406:
9385:
9382:
9381:
9360:
9355:
9347:
9344:
9343:
9322:
9319:
9318:
9297:
9292:
9284:
9281:
9280:
9262:
9259:
9258:
9240:
9237:
9236:
9212:
9207:
9199:
9196:
9195:
9177:
9174:
9173:
9155:
9152:
9151:
9150:then says that
9127:
9122:
9114:
9111:
9110:
9092:
9089:
9088:
9070:
9065:
9060:
9057:
9056:
9053:
9024:
9021:
9020:
9002:
8999:
8998:
8974:
8971:
8970:
8952:
8949:
8948:
8924:
8921:
8920:
8899:
8891:
8888:
8887:
8860:
8845:
8838:
8833:
8830:
8829:
8828:is realized as
8804:
8801:
8800:
8782:
8779:
8778:
8760:
8757:
8756:
8732:
8729:
8728:
8707:
8696:
8693:
8692:
8674:
8671:
8670:
8649:
8641:
8638:
8637:
8619:
8616:
8615:
8591:
8565:
8554:
8551:
8550:
8502:
8499:
8498:
8466:
8463:
8462:
8412:
8409:
8408:
8378:
8375:
8374:
8356:
8353:
8352:
8327:
8324:
8323:
8305:
8302:
8301:
8280:
8277:
8276:
8258:
8255:
8254:
8251:
8167:
8164:
8163:
8145:
8142:
8141:
8117:
8114:
8113:
8095:
8092:
8091:
8069:
8066:
8065:
8047:
8044:
8043:
7923:
7920:
7919:
7898:
7895:
7894:
7867:
7864:
7863:
7845:
7842:
7841:
7815:
7812:
7811:
7793:
7790:
7789:
7770:
7766:
7764:
7761:
7760:
7742:
7737:
7734:
7733:
7715:
7712:
7711:
7690:
7687:
7686:
7581:
7578:
7577:
7551:
7548:
7547:
7529:
7526:
7525:
7402:
7399:
7398:
7263:
7260:
7259:
7214:
7211:
7210:
7171:
7168:
7167:
7134:
7131:
7130:
7112:
7109:
7108:
7090:
7087:
7086:
7014:
7011:
7010:
6976:
6972:
6949:
6946:
6945:
6911:
6907:
6884:
6881:
6880:
6862:
6859:
6858:
6818:
6814:
6769:
6765:
6720:
6716:
6693:
6690:
6689:
6632:
6629:
6628:
6607:
6604:
6603:
6585:
6582:
6581:
6563:
6560:
6559:
6523:
6520:
6519:
6501:
6498:
6497:
6479:
6476:
6475:
6457:
6454:
6453:
6435:
6432:
6431:
6413:
6410:
6409:
6391:
6388:
6387:
6351:
6348:
6347:
6325:
6322:
6321:
6303:
6300:
6299:
6272:
6269:
6268:
6243:
6240:
6239:
6221:
6218:
6217:
6052:
6049:
6048:
6030:
6027:
6026:
6008:
6005:
6004:
5974:
5971:
5970:
5952:
5949:
5948:
5921:
5918:
5917:
5899:
5896:
5895:
5865:
5862:
5861:
5843:
5840:
5839:
5821:
5818:
5817:
5799:
5796:
5795:
5777:
5774:
5773:
5755:
5752:
5751:
5697:
5694:
5693:
5675:
5672:
5671:
5640:
5637:
5636:
5606:
5603:
5602:
5557:
5554:
5553:
5484:
5481:
5480:
5408:
5405:
5404:
5385:
5381:
5363:
5359:
5333:
5330:
5329:
5311:
5308:
5307:
5286:
5283:
5282:
5264:
5261:
5260:
5242:
5239:
5238:
5220:
5217:
5216:
5189:
5186:
5185:
5167:
5164:
5163:
5145:
5142:
5141:
5114:
5111:
5110:
5051:
5048:
5047:
5023:
5020:
5019:
5001:
4998:
4997:
4973:
4970:
4969:
4966:
4943:
4940:
4939:
4909:
4906:
4905:
4887:
4884:
4883:
4814:
4811:
4810:
4786:
4783:
4782:
4758:
4755:
4754:
4716:
4713:
4712:
4694:
4691:
4690:
4672:
4669:
4668:
4650:
4647:
4646:
4628:
4625:
4624:
4555:
4552:
4551:
4515:
4512:
4511:
4478:
4475:
4474:
4447:
4444:
4443:
4413:
4410:
4409:
4391:
4388:
4387:
4351:
4348:
4347:
4314:
4311:
4310:
4241:
4238:
4237:
4180:
4177:
4176:
4136:
4133:
4132:
4114:
4109:
4106:
4105:
4072:
4069:
4068:
4041:
4038:
4037:
4001:
3998:
3997:
3964:
3961:
3960:
3903:
3900:
3899:
3881:
3878:
3877:
3859:
3856:
3855:
3843:
3820:
3817:
3816:
3747:
3744:
3743:
3716:
3713:
3712:
3694:
3691:
3690:
3657:
3654:
3653:
3652:. For example,
3635:
3632:
3631:
3613:
3610:
3609:
3576:
3573:
3572:
3554:
3551:
3550:
3549:might take us,
3532:
3529:
3528:
3510:
3507:
3506:
3473:
3470:
3469:
3451:
3448:
3447:
3429:
3426:
3425:
3401:
3398:
3397:
3379:
3376:
3375:
3357:
3354:
3353:
3329:
3326:
3325:
3300:
3297:
3296:
3278:
3275:
3274:
3256:
3253:
3252:
3234:
3231:
3230:
3212:
3209:
3208:
3190:
3187:
3186:
3168:
3165:
3164:
3162:
3160:
3158:
3140:
3137:
3136:
3118:
3115:
3114:
3096:
3093:
3092:
3074:
3071:
3070:
3052:
3049:
3048:
3030:
3027:
3026:
3024:
3000:
2997:
2996:
2972:
2969:
2968:
2958:
2874:
2871:
2870:
2805:
2802:
2801:
2748:
2740:
2737:
2736:
2671:
2668:
2667:
2632:
2629:
2628:
2596:
2593:
2592:
2541:
2538:
2537:
2534:
2511:
2508:
2507:
2477:
2474:
2473:
2455:
2452:
2451:
2433:
2430:
2429:
2411:
2408:
2407:
2389:
2386:
2385:
2367:
2364:
2363:
2361:
2339:
2330:
2329:
2312:
2307:
2304:
2303:
2301:
2283:
2280:
2279:
2261:
2258:
2257:
2239:
2236:
2235:
2217:
2214:
2213:
2195:
2192:
2191:
2173:
2170:
2169:
2167:
2149:
2146:
2145:
2127:
2124:
2123:
2105:
2102:
2101:
2083:
2080:
2079:
2061:
2058:
2057:
2039:
2036:
2035:
2033:
2015:
2012:
2011:
2005:
1979:
1976:
1975:
1957:
1954:
1953:
1872:
1869:
1868:
1803:
1800:
1799:
1746:
1738:
1735:
1734:
1669:
1666:
1665:
1630:
1627:
1626:
1597:
1594:
1593:
1561:
1558:
1557:
1538:
1535:
1534:
1510:
1507:
1506:
1481:
1478:
1477:
1458:
1455:
1454:
1400:
1397:
1396:
1389:
1366:
1361:
1358:
1357:
1356:, definable as
1331:
1328:
1327:
1305:
1302:
1301:
1283:
1280:
1279:
1257:
1252:
1249:
1248:
1230:
1227:
1226:
1208:
1205:
1204:
1178:
1177:
1172:
1169:
1168:
1150:
1147:
1146:
1128:
1125:
1124:
1103:
1098:
1095:
1094:
1070:
1067:
1066:
1065:, also written
1038:
1035:
1034:
1016:
1013:
1012:
994:
991:
990:
978:) quantifiers.
961:
958:
957:
939:
936:
935:
887:
884:
883:
835:
832:
831:
809:
806:
805:
787:
784:
783:
765:
762:
761:
743:
740:
739:
712:
709:
708:
690:
687:
686:
668:
665:
664:
646:
643:
642:
624:
621:
620:
593:
590:
589:
561:
558:
557:
533:
530:
529:
511:
508:
507:
489:
486:
485:
466:
463:
462:
444:
441:
440:
421:
418:
417:
415:modal operators
408:
361:
344:
341:
340:
321:
319:
316:
315:
296:
293:
292:
273:
270:
269:
249:
244:
241:
240:
218:
215:
214:
195:
190:
187:
186:
153:
150:
149:
116:
113:
112:
79:
71:
60:
58:
55:
54:
21:
12:
11:
5:
10391:
10381:
10380:
10375:
10370:
10356:
10355:
10349:
10339:
10331:
10330:External links
10328:
10327:
10326:
10316:
10310:
10298:
10295:
10292:
10291:
10284:
10261:
10254:
10229:
10228:
10226:
10223:
10222:
10221:
10210:
10209:
10197:
10194:
10192:
10191:
10186:
10181:
10176:
10174:Temporal logic
10171:
10169:Kleene algebra
10166:
10160:
10158:
10155:
10143:temporal logic
10133:
10130:
10111:
10108:
10105:
10102:
10099:
10096:
10093:
10071:
10068:
10065:
10062:
10040:
10037:
10034:
10031:
10028:
10025:
10022:
10003:logical system
9988:
9985:
9982:
9979:
9976:
9973:
9951:
9948:
9945:
9942:
9939:
9919:
9916:
9869:
9866:
9863:
9860:
9857:
9846:Richard Ladner
9804:
9801:
9798:
9795:
9792:
9789:
9786:
9783:
9780:
9777:
9774:
9771:
9749:
9746:
9743:
9721:
9718:
9715:
9712:
9709:
9687:
9665:
9662:
9659:
9637:
9615:
9612:
9609:
9606:
9603:
9600:
9597:
9594:
9591:
9588:
9585:
9582:
9566:
9563:
9554:possible world
9549:
9546:
9532:
9528:
9525:
9522:
9519:
9516:
9513:
9510:
9506:
9502:
9499:
9495:
9491:
9488:
9468:
9448:
9420:
9417:
9414:
9392:
9389:
9367:
9363:
9358:
9354:
9351:
9329:
9326:
9304:
9300:
9295:
9291:
9288:
9266:
9244:
9222:
9219:
9215:
9210:
9206:
9203:
9181:
9159:
9137:
9134:
9130:
9125:
9121:
9118:
9096:
9073:
9068:
9064:
9052:
9049:
9034:
9031:
9028:
9006:
8984:
8981:
8978:
8956:
8934:
8931:
8928:
8906:
8902:
8898:
8895:
8873:
8870:
8867:
8863:
8858:
8855:
8852:
8848:
8844:
8841:
8837:
8824:The construct
8808:
8786:
8764:
8742:
8739:
8736:
8714:
8710:
8706:
8703:
8700:
8678:
8656:
8652:
8648:
8645:
8623:
8601:
8598:
8594:
8590:
8587:
8584:
8581:
8578:
8575:
8572:
8568:
8564:
8561:
8558:
8545:The construct
8530:
8527:
8524:
8521:
8518:
8515:
8512:
8509:
8506:
8479:
8476:
8473:
8470:
8446:
8443:
8440:
8437:
8434:
8431:
8428:
8425:
8422:
8419:
8416:
8385:
8382:
8360:
8334:
8331:
8309:
8287:
8284:
8262:
8250:
8247:
8228:
8225:
8222:
8219:
8216:
8213:
8210:
8207:
8204:
8201:
8198:
8195:
8192:
8189:
8186:
8183:
8180:
8177:
8174:
8171:
8149:
8127:
8124:
8121:
8099:
8088:natural number
8073:
8051:
8029:
8026:
8023:
8020:
8017:
8014:
8011:
8008:
8005:
8002:
7999:
7996:
7993:
7990:
7987:
7984:
7981:
7978:
7975:
7972:
7969:
7966:
7963:
7960:
7957:
7954:
7951:
7948:
7945:
7942:
7939:
7936:
7933:
7930:
7927:
7902:
7880:
7877:
7874:
7871:
7849:
7819:
7797:
7773:
7769:
7745:
7741:
7719:
7697:
7694:
7669:
7666:
7663:
7660:
7657:
7654:
7651:
7648:
7645:
7642:
7639:
7636:
7633:
7630:
7627:
7624:
7621:
7618:
7615:
7612:
7609:
7606:
7603:
7600:
7597:
7594:
7591:
7588:
7585:
7555:
7533:
7508:
7505:
7502:
7499:
7496:
7493:
7490:
7487:
7484:
7481:
7478:
7475:
7472:
7469:
7466:
7463:
7460:
7457:
7454:
7451:
7448:
7445:
7442:
7439:
7436:
7433:
7430:
7427:
7424:
7421:
7418:
7415:
7412:
7409:
7406:
7384:
7381:
7378:
7375:
7372:
7369:
7366:
7363:
7360:
7357:
7354:
7351:
7348:
7345:
7342:
7339:
7336:
7333:
7330:
7327:
7324:
7321:
7318:
7315:
7312:
7309:
7306:
7303:
7300:
7297:
7294:
7291:
7288:
7285:
7282:
7279:
7276:
7273:
7270:
7267:
7245:
7242:
7239:
7236:
7233:
7230:
7227:
7224:
7221:
7218:
7196:
7193:
7190:
7187:
7184:
7181:
7178:
7175:
7153:
7150:
7147:
7144:
7141:
7138:
7116:
7094:
7072:
7069:
7066:
7063:
7060:
7057:
7054:
7051:
7048:
7045:
7042:
7039:
7036:
7033:
7030:
7027:
7024:
7021:
7018:
6996:
6993:
6990:
6987:
6984:
6979:
6975:
6971:
6968:
6965:
6962:
6959:
6956:
6953:
6931:
6928:
6925:
6922:
6919:
6914:
6910:
6906:
6903:
6900:
6897:
6894:
6891:
6888:
6866:
6844:
6841:
6838:
6835:
6832:
6829:
6826:
6821:
6817:
6813:
6810:
6807:
6804:
6801:
6798:
6795:
6792:
6789:
6786:
6783:
6780:
6777:
6772:
6768:
6764:
6761:
6758:
6755:
6752:
6749:
6746:
6743:
6740:
6737:
6734:
6731:
6728:
6723:
6719:
6715:
6712:
6709:
6706:
6703:
6700:
6697:
6675:
6672:
6669:
6666:
6663:
6660:
6657:
6654:
6651:
6648:
6645:
6642:
6639:
6636:
6611:
6589:
6567:
6545:
6542:
6539:
6536:
6533:
6530:
6527:
6505:
6483:
6461:
6439:
6417:
6395:
6373:
6370:
6367:
6364:
6361:
6358:
6355:
6329:
6307:
6285:
6282:
6279:
6276:
6247:
6225:
6203:
6200:
6197:
6194:
6191:
6188:
6185:
6182:
6179:
6176:
6173:
6170:
6167:
6164:
6161:
6158:
6155:
6152:
6149:
6146:
6143:
6140:
6137:
6134:
6131:
6128:
6125:
6122:
6119:
6116:
6113:
6110:
6107:
6104:
6101:
6098:
6095:
6092:
6089:
6086:
6083:
6080:
6077:
6074:
6071:
6068:
6065:
6062:
6059:
6056:
6034:
6012:
5990:
5987:
5984:
5981:
5978:
5956:
5934:
5931:
5928:
5925:
5903:
5875:
5872:
5869:
5847:
5825:
5803:
5781:
5759:
5737:
5734:
5731:
5728:
5725:
5722:
5719:
5716:
5713:
5710:
5707:
5704:
5701:
5679:
5650:
5647:
5644:
5622:
5619:
5616:
5613:
5610:
5588:
5585:
5582:
5579:
5576:
5573:
5570:
5567:
5564:
5561:
5539:
5536:
5533:
5530:
5527:
5524:
5521:
5518:
5515:
5512:
5509:
5506:
5503:
5500:
5497:
5494:
5491:
5488:
5463:
5460:
5457:
5454:
5451:
5448:
5445:
5442:
5439:
5436:
5433:
5430:
5427:
5424:
5421:
5418:
5415:
5412:
5388:
5384:
5380:
5377:
5374:
5371:
5366:
5362:
5358:
5355:
5352:
5349:
5346:
5343:
5340:
5337:
5315:
5306:, replaced by
5293:
5290:
5268:
5246:
5224:
5202:
5199:
5196:
5193:
5171:
5149:
5127:
5124:
5121:
5118:
5094:
5091:
5088:
5085:
5082:
5079:
5076:
5073:
5070:
5067:
5064:
5061:
5058:
5055:
5027:
5005:
4983:
4980:
4977:
4965:
4962:
4947:
4925:
4922:
4919:
4916:
4913:
4891:
4869:
4866:
4863:
4860:
4857:
4854:
4851:
4848:
4845:
4842:
4839:
4836:
4833:
4830:
4827:
4824:
4821:
4818:
4796:
4793:
4790:
4768:
4765:
4762:
4732:
4729:
4726:
4723:
4720:
4698:
4676:
4654:
4632:
4610:
4607:
4604:
4601:
4598:
4595:
4592:
4589:
4586:
4583:
4580:
4577:
4574:
4571:
4568:
4565:
4562:
4559:
4534:
4531:
4528:
4525:
4522:
4519:
4497:
4494:
4491:
4488:
4485:
4482:
4460:
4457:
4454:
4451:
4429:
4426:
4423:
4420:
4417:
4408:must hold but
4395:
4373:
4370:
4367:
4364:
4361:
4358:
4355:
4333:
4330:
4327:
4324:
4321:
4318:
4296:
4293:
4290:
4287:
4284:
4281:
4278:
4275:
4272:
4269:
4266:
4263:
4260:
4257:
4254:
4251:
4248:
4245:
4223:
4220:
4217:
4214:
4211:
4208:
4205:
4202:
4199:
4196:
4193:
4190:
4187:
4184:
4175:The inference
4158:
4155:
4152:
4149:
4146:
4143:
4140:
4117:
4113:
4091:
4088:
4085:
4082:
4079:
4076:
4054:
4051:
4048:
4045:
4023:
4020:
4017:
4014:
4011:
4008:
4005:
3983:
3980:
3977:
3974:
3971:
3968:
3946:
3943:
3940:
3937:
3934:
3931:
3928:
3925:
3922:
3919:
3916:
3913:
3910:
3907:
3885:
3863:
3842:
3839:
3824:
3802:
3799:
3796:
3793:
3790:
3787:
3784:
3781:
3778:
3775:
3772:
3769:
3766:
3763:
3760:
3757:
3754:
3751:
3729:
3726:
3723:
3720:
3698:
3676:
3673:
3670:
3667:
3664:
3661:
3639:
3617:
3595:
3592:
3589:
3586:
3583:
3580:
3558:
3536:
3514:
3492:
3489:
3486:
3483:
3480:
3477:
3455:
3433:
3411:
3408:
3405:
3383:
3361:
3339:
3336:
3333:
3304:
3282:
3260:
3238:
3216:
3194:
3185:by performing
3172:
3144:
3122:
3100:
3091:, then either
3078:
3056:
3034:
3010:
3007:
3004:
2982:
2979:
2976:
2938:
2935:
2932:
2929:
2926:
2923:
2920:
2917:
2914:
2911:
2908:
2905:
2902:
2899:
2896:
2893:
2890:
2887:
2884:
2881:
2878:
2854:
2851:
2848:
2845:
2842:
2839:
2836:
2833:
2830:
2827:
2824:
2821:
2818:
2815:
2812:
2809:
2785:
2782:
2779:
2776:
2773:
2770:
2767:
2764:
2761:
2758:
2755:
2751:
2747:
2744:
2720:
2717:
2714:
2711:
2708:
2705:
2702:
2699:
2696:
2693:
2690:
2687:
2684:
2681:
2678:
2675:
2651:
2648:
2645:
2642:
2639:
2636:
2612:
2609:
2606:
2603:
2600:
2575:
2572:
2569:
2566:
2563:
2560:
2557:
2554:
2551:
2548:
2545:
2533:
2530:
2515:
2481:
2459:
2437:
2415:
2393:
2371:
2358:Kleene algebra
2342:
2338:
2333:
2328:
2325:
2322:
2319:
2315:
2311:
2287:
2265:
2243:
2221:
2199:
2177:
2153:
2131:
2109:
2087:
2065:
2043:
2019:
1983:
1961:
1933:
1930:
1927:
1924:
1921:
1918:
1915:
1912:
1909:
1906:
1903:
1900:
1897:
1894:
1891:
1888:
1885:
1882:
1879:
1876:
1852:
1849:
1846:
1843:
1840:
1837:
1834:
1831:
1828:
1825:
1822:
1819:
1816:
1813:
1810:
1807:
1783:
1780:
1777:
1774:
1771:
1768:
1765:
1762:
1759:
1756:
1753:
1749:
1745:
1742:
1718:
1715:
1712:
1709:
1706:
1703:
1700:
1697:
1694:
1691:
1688:
1685:
1682:
1679:
1676:
1673:
1649:
1646:
1643:
1640:
1637:
1634:
1610:
1607:
1604:
1601:
1577:
1574:
1571:
1568:
1565:
1545:
1542:
1517:
1514:
1494:
1491:
1488:
1485:
1465:
1462:
1434:
1431:
1428:
1425:
1422:
1419:
1416:
1413:
1410:
1407:
1404:
1388:
1385:
1369:
1365:
1335:
1309:
1287:
1260:
1256:
1234:
1212:
1186:
1181:
1176:
1154:
1132:
1110:
1106:
1102:
1080:
1077:
1074:
1048:
1045:
1042:
1020:
998:
965:
943:
921:
918:
915:
912:
909:
906:
903:
900:
897:
894:
891:
869:
866:
863:
860:
857:
854:
851:
848:
845:
842:
839:
813:
791:
769:
747:
725:
722:
719:
716:
694:
672:
650:
628:
606:
603:
600:
597:
571:
568:
565:
543:
540:
537:
515:
493:
473:
470:
448:
428:
425:
407:
404:
367:
364:
360:
357:
354:
351:
348:
327:
324:
300:
277:
252:
248:
228:
225:
222:
202:
198:
194:
166:
163:
160:
157:
129:
126:
123:
120:
98:
97:
86:
78:
70:
67:
9:
6:
4:
3:
2:
10390:
10379:
10376:
10374:
10371:
10369:
10366:
10365:
10363:
10353:
10350:
10347:
10343:
10340:
10337:
10334:
10333:
10324:
10320:
10317:
10314:
10311:
10308:
10304:
10303:Vaughan Pratt
10301:
10300:
10287:
10281:
10274:
10273:
10265:
10257:
10251:
10247:
10243:
10242:
10234:
10230:
10219:
10216:
10212:
10211:
10207:
10203:
10200:
10199:
10190:
10187:
10185:
10182:
10180:
10177:
10175:
10172:
10170:
10167:
10165:
10162:
10161:
10154:
10152:
10148:
10144:
10140:
10129:
10127:
10106:
10103:
10100:
10094:
10091:
10069:
10063:
10035:
10032:
10029:
10023:
10020:
10012:
10008:
10004:
9986:
9980:
9971:
9949:
9943:
9937:
9929:
9925:
9924:Vaughan Pratt
9915:
9913:
9909:
9905:
9900:
9899:Vaughan Pratt
9896:
9892:
9888:
9883:
9867:
9864:
9861:
9858:
9855:
9847:
9843:
9838:
9836:
9832:
9828:
9824:
9820:
9799:
9796:
9793:
9784:
9781:
9778:
9775:
9772:
9747:
9744:
9741:
9719:
9716:
9713:
9710:
9707:
9685:
9663:
9660:
9657:
9635:
9610:
9607:
9604:
9595:
9592:
9589:
9586:
9583:
9572:
9562:
9560:
9555:
9545:
9530:
9523:
9520:
9517:
9514:
9511:
9504:
9497:
9493:
9489:
9466:
9446:
9438:
9434:
9418:
9415:
9412:
9390:
9361:
9356:
9352:
9327:
9298:
9293:
9289:
9264:
9242:
9220:
9213:
9208:
9204:
9179:
9157:
9135:
9128:
9123:
9119:
9094:
9071:
9066:
9062:
9048:
9032:
9029:
9004:
8982:
8979:
8954:
8947:. As long as
8932:
8929:
8904:
8900:
8896:
8893:
8871:
8868:
8861:
8856:
8850:
8846:
8842:
8839:
8827:
8822:
8806:
8784:
8777:. Hence when
8762:
8740:
8737:
8734:
8712:
8708:
8704:
8701:
8676:
8654:
8650:
8646:
8643:
8621:
8596:
8592:
8588:
8585:
8576:
8570:
8566:
8562:
8559:
8548:
8543:
8528:
8525:
8522:
8516:
8510:
8507:
8497:
8493:
8474:
8471:
8459:
8441:
8435:
8426:
8420:
8417:
8407:
8403:
8401:
8383:
8380:
8358:
8350:
8332:
8329:
8307:
8285:
8282:
8260:
8246:
8244:
8226:
8220:
8217:
8205:
8199:
8190:
8181:
8178:
8172:
8169:
8147:
8125:
8122:
8119:
8097:
8089:
8071:
8049:
8024:
8021:
8018:
8009:
7991:
7988:
7985:
7982:
7979:
7964:
7961:
7958:
7946:
7940:
7934:
7917:
7900:
7875:
7847:
7839:
7835:
7817:
7795:
7771:
7767:
7743:
7739:
7717:
7695:
7683:
7664:
7655:
7637:
7634:
7631:
7616:
7604:
7598:
7592:
7575:
7571:
7553:
7531:
7522:
7503:
7500:
7497:
7488:
7470:
7467:
7464:
7461:
7458:
7443:
7440:
7437:
7425:
7419:
7413:
7379:
7376:
7373:
7364:
7346:
7343:
7340:
7328:
7325:
7322:
7319:
7316:
7304:
7301:
7298:
7286:
7280:
7274:
7240:
7234:
7231:
7228:
7225:
7222:
7191:
7188:
7185:
7176:
7148:
7145:
7142:
7114:
7092:
7067:
7058:
7052:
7049:
7046:
7043:
7040:
7031:
7028:
7025:
7022:
7019:
6991:
6977:
6969:
6966:
6963:
6960:
6957:
6926:
6912:
6904:
6901:
6898:
6895:
6892:
6864:
6842:
6839:
6833:
6819:
6811:
6808:
6805:
6802:
6799:
6790:
6784:
6770:
6762:
6759:
6756:
6753:
6750:
6741:
6735:
6721:
6713:
6710:
6707:
6704:
6701:
6670:
6658:
6652:
6649:
6646:
6643:
6640:
6625:
6609:
6587:
6565:
6540:
6537:
6534:
6531:
6528:
6503:
6481:
6459:
6437:
6415:
6393:
6368:
6365:
6362:
6359:
6356:
6345:
6327:
6305:
6280:
6265:
6263:
6245:
6223:
6198:
6186:
6180:
6177:
6174:
6171:
6168:
6147:
6135:
6132:
6129:
6126:
6123:
6111:
6096:
6090:
6087:
6084:
6081:
6078:
6069:
6063:
6032:
6010:
5988:
5985:
5982:
5979:
5976:
5954:
5947:, the action
5929:
5901:
5893:
5889:
5873:
5870:
5867:
5845:
5823:
5801:
5779:
5757:
5735:
5732:
5729:
5723:
5717:
5714:
5711:
5708:
5705:
5677:
5668:
5666:
5648:
5645:
5642:
5620:
5617:
5614:
5611:
5608:
5586:
5583:
5580:
5574:
5571:
5568:
5565:
5562:
5537:
5534:
5531:
5528:
5525:
5516:
5513:
5510:
5501:
5498:
5495:
5492:
5489:
5479:The instance
5477:
5461:
5458:
5455:
5452:
5449:
5440:
5437:
5434:
5431:
5428:
5419:
5416:
5413:
5386:
5382:
5378:
5375:
5364:
5360:
5356:
5353:
5344:
5341:
5338:
5313:
5291:
5244:
5197:
5169:
5122:
5107:
5089:
5074:
5062:
5059:
5056:
5046:
5042:
5025:
5003:
4981:
4978:
4975:
4961:
4945:
4923:
4920:
4917:
4914:
4911:
4889:
4864:
4861:
4858:
4849:
4846:
4843:
4840:
4837:
4825:
4822:
4819:
4791:
4763:
4752:
4748:
4730:
4727:
4724:
4721:
4718:
4696:
4674:
4652:
4630:
4605:
4602:
4599:
4590:
4587:
4584:
4581:
4578:
4566:
4563:
4560:
4548:
4532:
4526:
4517:
4495:
4489:
4480:
4458:
4452:
4427:
4421:
4418:
4393:
4371:
4365:
4362:
4353:
4331:
4325:
4316:
4291:
4285:
4282:
4273:
4261:
4255:
4246:
4221:
4215:
4212:
4203:
4200:
4197:
4191:
4182:
4173:
4156:
4150:
4147:
4138:
4115:
4111:
4089:
4083:
4074:
4052:
4046:
4021:
4015:
4012:
4003:
3981:
3975:
3966:
3944:
3938:
3935:
3926:
3923:
3920:
3914:
3905:
3883:
3861:
3852:
3851:necessitation
3848:
3838:
3822:
3797:
3794:
3791:
3782:
3779:
3776:
3773:
3770:
3758:
3755:
3752:
3727:
3721:
3696:
3674:
3668:
3659:
3637:
3615:
3593:
3587:
3578:
3556:
3534:
3512:
3490:
3484:
3478:
3475:
3453:
3431:
3409:
3406:
3403:
3381:
3359:
3337:
3331:
3322:
3318:
3302:
3280:
3258:
3236:
3214:
3192:
3170:
3142:
3120:
3098:
3076:
3054:
3032:
3005:
2977:
2966:
2962:
2956:
2951:
2933:
2927:
2921:
2918:
2906:
2903:
2897:
2894:
2888:
2882:
2879:
2867:
2852:
2846:
2843:
2834:
2828:
2825:
2819:
2813:
2810:
2798:
2783:
2777:
2768:
2759:
2753:
2749:
2745:
2733:
2718:
2712:
2706:
2703:
2697:
2688:
2682:
2679:
2676:
2664:
2649:
2643:
2637:
2625:
2610:
2604:
2589:
2573:
2564:
2552:
2546:
2529:
2513:
2505:
2501:
2500:n := n+1
2497:
2479:
2457:
2435:
2413:
2391:
2369:
2359:
2340:
2336:
2331:
2326:
2323:
2320:
2317:
2313:
2309:
2285:
2263:
2241:
2219:
2197:
2175:
2151:
2129:
2107:
2085:
2063:
2041:
2017:
2009:
2006:A2 says that
2003:
1999:
1981:
1959:
1951:
1946:
1931:
1925:
1922:
1910:
1904:
1895:
1886:
1883:
1877:
1874:
1865:
1850:
1844:
1841:
1832:
1826:
1823:
1817:
1811:
1808:
1796:
1781:
1775:
1766:
1757:
1751:
1747:
1743:
1731:
1716:
1710:
1704:
1701:
1695:
1686:
1680:
1677:
1674:
1662:
1647:
1641:
1635:
1623:
1608:
1602:
1590:
1575:
1569:
1563:
1543:
1540:
1532:
1531:necessitation
1515:
1512:
1492:
1486:
1483:
1463:
1460:
1452:
1451:
1432:
1423:
1411:
1405:
1394:
1384:
1367:
1363:
1355:
1351:
1333:
1325:
1307:
1285:
1277:
1258:
1254:
1232:
1210:
1202:
1184:
1179:
1174:
1152:
1130:
1108:
1100:
1078:
1075:
1072:
1064:
1046:
1043:
1040:
1018:
996:
988:
984:
979:
919:
910:
898:
892:
867:
858:
846:
840:
829:
811:
789:
767:
745:
723:
717:
692:
670:
648:
626:
604:
598:
587:
566:
538:
513:
491:
471:
468:
446:
426:
423:
416:
412:
403:
401:
397:
393:
389:
384:
382:
365:
362:
355:
346:
325:
322:
314:
313:postcondition
298:
291:
275:
267:
250:
246:
226:
223:
220:
200:
196:
192:
184:
180:
164:
158:
147:
143:
127:
121:
110:
106:
101:
84:
53:
52:
51:
48:
46:
42:
38:
37:dynamic logic
34:
30:
26:
19:
10345:
10323:Dexter Kozen
10271:
10264:
10240:
10233:
10206:Dexter Kozen
10135:
9921:
9884:
9839:
9834:
9830:
9826:
9569:Ordinary or
9568:
9551:
9435:
9054:
8826:while p do a
8825:
8823:
8546:
8544:
8495:
8494:
8460:
8405:
8404:
8399:
8348:
8252:
8242:
8087:
7915:
7837:
7833:
7684:
7523:
6626:
6266:
6261:
5890:
5669:
5478:
5108:
5044:
5043:
4967:
4750:
4746:
4549:
4174:
3850:
3847:modus ponens
3846:
3844:
3323:
3319:
2964:
2960:
2954:
2952:
2868:
2799:
2734:
2665:
2626:
2590:
2535:
2503:
2499:
2032:into itself.
2007:
2001:
1997:
1952:terminates,
1949:
1947:
1866:
1797:
1732:
1663:
1624:
1591:
1530:
1450:modus ponens
1448:
1390:
1353:
1349:
1323:
1275:
1200:
1062:
980:
409:
385:
290:precondition
182:
178:
145:
141:
108:
105:propositions
104:
102:
99:
49:
36:
22:
10368:Modal logic
10319:David Harel
10313:David Harel
10202:David Harel
10164:Hoare logic
10139:Amir Pnueli
9928:Hoare logic
8636:holds then
8086:is of type
2532:Derivations
1393:modal logic
411:Modal logic
392:linguistics
381:Hoare logic
41:modal logic
10362:Categories
10297:References
10285:8301068590
10255:013215871X
9700:are data,
9194:to, while
8691:, whereas
8373:is false,
8347:acts as a
8275:an action
8245:be false.
7836:, or even
7572:to obtain
5403:, or with
4964:Assignment
4346:holds but
396:philosophy
29:philosophy
10225:Footnotes
10095:
10024:
9975:→
9797:≥
9745:≥
9608:≥
9531:∗
9388:∃
9366:⟩
9350:⟨
9325:∀
9218:⟩
9202:⟨
9027:¬
8977:¬
8927:¬
8866:¬
8857:∗
8738:∪
8699:¬
8583:¬
8577:∪
8526:∧
8520:↔
8514:⟩
8505:⟨
8478:⟩
8469:⟨
8439:→
8430:↔
8221:∗
8212:↔
8194:→
8182:∗
8173:∧
8013:Φ
8007:∀
8004:→
7974:Φ
7971:→
7953:Φ
7944:∀
7941:∧
7929:Φ
7870:Φ
7744:∗
7693:∀
7659:Φ
7653:∀
7650:→
7626:Φ
7623:→
7611:Φ
7602:∀
7599:∧
7587:Φ
7492:Φ
7486:∀
7483:→
7453:Φ
7450:→
7432:Φ
7423:∀
7420:∧
7408:Φ
7368:Φ
7362:∀
7359:→
7335:Φ
7311:→
7293:Φ
7284:∀
7281:∧
7269:Φ
7241:∗
7180:Φ
7174:∀
7137:Φ
7085:, having
7062:Φ
7059:…
6986:Φ
6921:Φ
6843:…
6840:∧
6828:Φ
6791:∧
6779:Φ
6742:∧
6730:Φ
6665:Φ
6659:∗
6275:Φ
6193:Φ
6187:∗
6160:→
6142:Φ
6118:→
6106:Φ
6097:∗
6070:∧
6058:Φ
5924:Φ
5871:≤
5727:⟩
5724:∗
5700:⟨
5678:∗
5646:≥
5618:≥
5584:≥
5535:≥
5523:↔
5514:≥
5447:↔
5373:↔
5289:∀
5267:Φ
5223:Φ
5192:Φ
5148:Φ
5117:Φ
5084:Φ
5081:↔
5069:Φ
4862:≥
4853:⟩
4835:⟨
4832:→
4823:≥
4795:⟩
4789:⟨
4603:≥
4573:→
4564:≥
4521:→
4484:→
4422:∗
4366:∗
4357:→
4320:→
4286:∗
4277:→
4268:→
4250:→
4216:∗
4207:→
4201:⊢
4186:→
4151:∗
4142:→
4116:∗
4078:→
4016:∗
4007:→
3970:→
3939:∗
3930:→
3924:⊢
3909:→
3765:→
3663:→
3582:→
3479:⊢
3407:⊢
3335:→
3009:⟩
3003:⟨
2931:⟩
2925:⟨
2922:∧
2916:¬
2910:⟩
2907:∗
2901:⟨
2898:∨
2892:→
2886:⟩
2883:∗
2877:⟨
2850:⟩
2847:∗
2841:⟨
2838:⟩
2832:⟨
2829:∨
2823:↔
2817:⟩
2814:∗
2808:⟨
2781:⟩
2775:⟨
2772:⟩
2766:⟨
2763:↔
2757:⟩
2743:⟨
2716:⟩
2710:⟨
2707:∨
2701:⟩
2695:⟨
2692:↔
2686:⟩
2680:∪
2674:⟨
2647:↔
2641:⟩
2635:⟨
2608:⟩
2602:⟨
2599:¬
2571:¬
2568:⟩
2562:⟨
2559:¬
2556:↔
2341:∗
2324:∪
2314:∗
2190:and then
2000:. (Thus
1926:∗
1917:→
1899:→
1887:∗
1878:∧
1845:∗
1827:∧
1821:↔
1812:∗
1761:↔
1705:∧
1690:↔
1678:∪
1645:↔
1564:⊢
1541:⊢
1513:⊢
1490:→
1484:⊢
1461:⊢
1430:¬
1427:⟩
1421:⟨
1418:¬
1415:↔
1368:∗
1276:iteration
1259:∗
1225:and then
1044:∪
964:∃
942:∀
917:¬
905:¬
902:↔
896:⟩
890:⟨
865:¬
862:⟩
856:⟨
853:¬
850:↔
721:⟩
715:⟨
570:⟩
564:⟨
469:◊
424:◻
363:φ
350:→
347:φ
323:φ
299:φ
251:∗
224:∪
162:⟩
156:⟨
66:→
10157:See also
10151:livelock
10147:deadlock
9889:at most
9437:Dijkstra
9342:, while
8398:acts as
1556:implies
1505:implies
1201:sequence
406:Language
366:′
326:′
73:It rains
10220:, 2007.
10053:, with
9918:History
7834:integer
2450:, then
2234:, then
2100:, then
109:actions
10282:
10252:
9908:Parikh
9904:Gabbay
9833:, and
9678:, and
9279:true.
6003:, and
4996:where
1529:) and
1387:Axioms
1063:choice
983:Kleene
311:, and
31:, and
10276:(PDF)
9912:Kozen
8400:BLOCK
7574:Peano
7009:into
6342:as a
4751:might
2955:BLOCK
2869:T6.
2800:T5.
2735:T4.
2666:T3.
2627:T2.
2591:T1.
2002:BLOCK
1998:false
1950:BLOCK
1867:A6.
1798:A5.
1733:A4.
1664:A3.
1625:A2.
1592:A1.
1324:BLOCK
25:logic
10348:site
10280:ISBN
10250:ISBN
10009:and
9844:and
9762:and
8492:is:
8249:Test
8243:must
7838:real
7546:for
6602:for
6298:for
6238:for
4781:and
4749:and
4747:must
3849:and
2995:and
1476:and
1350:SKIP
1011:and
882:and
828:dual
556:and
10344:at
10246:221
10092:wlp
9964:as
9835:not
9827:and
8496:T8.
8406:A8.
8349:NOP
6879:of
6025:as
5969:as
5663:by
5215:is
5045:A7.
3113:or
3047:or
2965:NOP
2961:NOP
2356:of
2056:or
2008:NOP
1589:).
1354:NOP
1352:or
1348:or
1322:or
1145:or
1093:or
985:'s
23:In
10364::
10321:,
10248:.
10204:,
10149:,
10021:wp
9859::=
9837:.
9831:or
9829:,
9776::=
9711::=
9650:,
9587::=
9515::=
9494::=
9433:.
9416::=
9357::=
9294::=
9209::=
9124::=
9067::=
9047:.
7521:.
7320::=
7226::=
7044::=
7023::=
6961::=
6896::=
6803::=
6754::=
6705::=
6644::=
6532::=
6360::=
6172::=
6127::=
6082::=
5980::=
5888:.
5709::=
5667:.
5566::=
5493::=
5417::=
5342::=
5060::=
4979::=
4938:,
4915::=
4841::=
4745:,
4722::=
4667:,
4582::=
3774::=
3317:.
2528:.
1274:,
1199:,
1061:,
400:AI
398:,
394:,
383:.
288:,
47:.
35:,
27:,
10288:.
10258:.
10110:)
10107:p
10104:,
10101:a
10098:(
10070:p
10067:]
10064:a
10061:[
10039:)
10036:p
10033:,
10030:a
10027:(
9987:q
9984:]
9981:a
9978:[
9972:p
9950:q
9947:}
9944:a
9941:{
9938:p
9868:1
9865:+
9862:x
9856:x
9803:)
9800:4
9794:x
9791:(
9788:]
9785:1
9782:+
9779:x
9773:x
9770:[
9748:4
9742:x
9720:1
9717:+
9714:x
9708:x
9686:4
9664:1
9661:+
9658:x
9636:x
9614:)
9611:4
9605:x
9602:(
9599:]
9596:1
9593:+
9590:x
9584:x
9581:[
9527:)
9524:1
9521:+
9518:x
9512:x
9509:(
9505:;
9501:)
9498:0
9490:x
9487:(
9467:x
9447:x
9419:?
9413:x
9391:x
9362:?
9353:x
9328:x
9303:]
9299:?
9290:x
9287:[
9265:p
9243:x
9221:p
9214:?
9205:x
9180:x
9158:p
9136:p
9133:]
9129:?
9120:x
9117:[
9095:x
9072:?
9063:x
9033:?
9030:p
9005:p
8983:?
8980:p
8955:p
8933:?
8930:p
8905:a
8901:;
8897:?
8894:p
8872:?
8869:p
8862:;
8854:)
8851:a
8847:;
8843:?
8840:p
8836:(
8807:p
8785:p
8763:a
8741:0
8735:a
8713:b
8709:;
8705:?
8702:p
8677:a
8655:a
8651:;
8647:?
8644:p
8622:p
8600:)
8597:b
8593:;
8589:?
8586:p
8580:(
8574:)
8571:a
8567:;
8563:?
8560:p
8557:(
8529:q
8523:p
8517:q
8511:?
8508:p
8475:?
8472:p
8445:)
8442:q
8436:p
8433:(
8427:q
8424:]
8421:?
8418:p
8415:[
8384:?
8381:p
8359:p
8333:?
8330:p
8308:p
8286:?
8283:p
8261:p
8227:p
8224:]
8218:a
8215:[
8209:)
8206:p
8203:]
8200:a
8197:[
8191:p
8188:(
8185:]
8179:a
8176:[
8170:p
8148:n
8126:i
8123:+
8120:n
8098:n
8072:n
8050:n
8028:)
8025:i
8022:+
8019:n
8016:(
8010:i
8001:)
7998:)
7995:)
7992:1
7989:+
7986:i
7983:+
7980:n
7977:(
7968:)
7965:i
7962:+
7959:n
7956:(
7950:(
7947:i
7938:)
7935:n
7932:(
7926:(
7901:n
7879:)
7876:n
7873:(
7848:n
7818:n
7796:i
7772:i
7768:a
7740:a
7718:i
7696:i
7668:)
7665:i
7662:(
7656:i
7647:)
7644:)
7641:)
7638:1
7635:+
7632:i
7629:(
7620:)
7617:i
7614:(
7608:(
7605:i
7596:)
7593:0
7590:(
7584:(
7554:n
7532:0
7507:)
7504:i
7501:+
7498:n
7495:(
7489:i
7480:)
7477:)
7474:)
7471:1
7468:+
7465:i
7462:+
7459:n
7456:(
7447:)
7444:i
7441:+
7438:n
7435:(
7429:(
7426:i
7417:)
7414:n
7411:(
7405:(
7383:)
7380:i
7377:+
7374:n
7371:(
7365:i
7356:)
7353:)
7350:)
7347:i
7344:+
7341:n
7338:(
7332:]
7329:1
7326:+
7323:n
7317:n
7314:[
7308:)
7305:i
7302:+
7299:n
7296:(
7290:(
7287:i
7278:)
7275:n
7272:(
7266:(
7244:]
7238:)
7235:1
7232:+
7229:n
7223:n
7220:(
7217:[
7195:)
7192:i
7189:+
7186:n
7183:(
7177:i
7152:)
7149:i
7146:+
7143:n
7140:(
7115:i
7093:i
7071:)
7068:n
7065:(
7056:]
7053:1
7050:+
7047:n
7041:n
7038:[
7035:]
7032:1
7029:+
7026:n
7020:n
7017:[
6995:)
6992:n
6989:(
6983:]
6978:i
6974:)
6970:1
6967:+
6964:n
6958:n
6955:(
6952:[
6930:)
6927:n
6924:(
6918:]
6913:i
6909:)
6905:1
6902:+
6899:n
6893:n
6890:(
6887:[
6865:i
6837:)
6834:n
6831:(
6825:]
6820:2
6816:)
6812:1
6809:+
6806:n
6800:n
6797:(
6794:[
6788:)
6785:n
6782:(
6776:]
6771:1
6767:)
6763:1
6760:+
6757:n
6751:n
6748:(
6745:[
6739:)
6736:n
6733:(
6727:]
6722:0
6718:)
6714:1
6711:+
6708:n
6702:n
6699:(
6696:[
6674:)
6671:n
6668:(
6662:]
6656:)
6653:1
6650:+
6647:n
6641:n
6638:(
6635:[
6610:n
6588:0
6566:n
6544:]
6541:1
6538:+
6535:n
6529:n
6526:[
6504:n
6482:n
6460:n
6438:a
6416:n
6394:n
6372:]
6369:1
6366:+
6363:n
6357:n
6354:[
6328:p
6306:p
6284:)
6281:n
6278:(
6246:n
6224:0
6202:)
6199:n
6196:(
6190:]
6184:)
6181:1
6178:+
6175:n
6169:n
6166:(
6163:[
6157:)
6154:)
6151:)
6148:n
6145:(
6139:]
6136:1
6133:+
6130:n
6124:n
6121:[
6115:)
6112:n
6109:(
6103:(
6100:]
6094:)
6091:1
6088:+
6085:n
6079:n
6076:(
6073:[
6067:)
6064:n
6061:(
6055:(
6033:0
6011:n
5989:1
5986:+
5983:n
5977:n
5955:a
5933:)
5930:n
5927:(
5902:p
5874:7
5868:x
5846:x
5824:x
5802:x
5780:x
5758:x
5736:7
5733:=
5730:x
5721:)
5718:1
5715:+
5712:x
5706:x
5703:(
5649:3
5643:x
5621:4
5615:1
5612:+
5609:x
5587:4
5581:x
5578:]
5575:1
5572:+
5569:x
5563:x
5560:[
5538:4
5532:1
5529:+
5526:x
5520:)
5517:4
5511:x
5508:(
5505:]
5502:1
5499:+
5496:x
5490:x
5487:[
5462:e
5459:+
5456:c
5453:=
5450:b
5444:)
5441:x
5438:+
5435:c
5432:=
5429:b
5426:(
5423:]
5420:e
5414:x
5411:[
5387:2
5383:y
5379:=
5376:e
5370:)
5365:2
5361:y
5357:=
5354:x
5351:(
5348:]
5345:e
5339:x
5336:[
5314:e
5292:x
5245:x
5201:)
5198:e
5195:(
5170:x
5126:)
5123:x
5120:(
5093:)
5090:e
5087:(
5078:)
5075:x
5072:(
5066:]
5063:e
5057:x
5054:[
5026:e
5004:x
4982:e
4976:x
4946:x
4924:1
4921:+
4918:x
4912:x
4890:x
4868:)
4865:4
4859:x
4856:(
4850:1
4847:+
4844:x
4838:x
4829:)
4826:3
4820:x
4817:(
4792:a
4767:]
4764:a
4761:[
4731:1
4728:+
4725:x
4719:x
4697:a
4675:x
4653:x
4631:x
4609:)
4606:4
4600:x
4597:(
4594:]
4591:1
4588:+
4585:x
4579:x
4576:[
4570:)
4567:3
4561:x
4558:(
4533:b
4530:]
4527:k
4524:[
4518:b
4496:b
4493:]
4490:k
4487:[
4481:b
4459:b
4456:]
4453:k
4450:[
4428:b
4425:]
4419:k
4416:[
4394:b
4372:b
4369:]
4363:k
4360:[
4354:b
4332:b
4329:]
4326:k
4323:[
4317:b
4295:)
4292:b
4289:]
4283:k
4280:[
4274:b
4271:(
4265:)
4262:b
4259:]
4256:k
4253:[
4247:b
4244:(
4222:b
4219:]
4213:k
4210:[
4204:b
4198:b
4195:]
4192:k
4189:[
4183:b
4157:b
4154:]
4148:k
4145:[
4139:b
4112:k
4090:b
4087:]
4084:k
4081:[
4075:b
4053:b
4050:]
4047:k
4044:[
4022:b
4019:]
4013:k
4010:[
4004:b
3982:b
3979:]
3976:k
3973:[
3967:b
3945:b
3942:]
3936:k
3933:[
3927:b
3921:b
3918:]
3915:k
3912:[
3906:b
3884:b
3862:k
3823:x
3801:)
3798:1
3795:=
3792:x
3789:(
3786:]
3783:1
3780:+
3777:x
3771:x
3768:[
3762:)
3759:1
3756:=
3753:x
3750:(
3728:p
3725:]
3722:a
3719:[
3697:p
3675:p
3672:]
3669:a
3666:[
3660:p
3638:a
3616:p
3594:p
3591:]
3588:a
3585:[
3579:p
3557:p
3535:a
3513:p
3491:p
3488:]
3485:a
3482:[
3476:p
3454:q
3432:p
3410:q
3404:p
3382:q
3360:p
3338:q
3332:p
3303:p
3281:a
3259:p
3237:a
3215:p
3193:a
3171:p
3157:.
3143:p
3121:b
3099:a
3077:p
3055:b
3033:a
3006:1
2981:]
2978:1
2975:[
2957:.
2937:)
2934:p
2928:a
2919:p
2913:(
2904:a
2895:p
2889:p
2880:a
2853:p
2844:a
2835:a
2826:p
2820:p
2811:a
2784:p
2778:b
2769:a
2760:p
2754:b
2750:;
2746:a
2719:p
2713:b
2704:p
2698:a
2689:p
2683:b
2677:a
2650:p
2644:p
2638:1
2611:p
2605:0
2574:p
2565:a
2553:p
2550:]
2547:a
2544:[
2514:a
2504:n
2480:a
2458:p
2436:a
2414:p
2392:a
2370:p
2360:.
2337:a
2332:;
2327:a
2321:1
2318:=
2310:a
2300:.
2286:p
2264:b
2242:a
2220:p
2198:b
2176:a
2152:b
2130:p
2108:a
2086:p
2064:b
2042:a
2018:p
1982:p
1960:p
1932:p
1929:]
1923:a
1920:[
1914:)
1911:p
1908:]
1905:a
1902:[
1896:p
1893:(
1890:]
1884:a
1881:[
1875:p
1851:p
1848:]
1842:a
1839:[
1836:]
1833:a
1830:[
1824:p
1818:p
1815:]
1809:a
1806:[
1782:p
1779:]
1776:b
1773:[
1770:]
1767:a
1764:[
1758:p
1755:]
1752:b
1748:;
1744:a
1741:[
1717:p
1714:]
1711:b
1708:[
1702:p
1699:]
1696:a
1693:[
1687:p
1684:]
1681:b
1675:a
1672:[
1648:p
1642:p
1639:]
1636:1
1633:[
1609:p
1606:]
1603:0
1600:[
1576:p
1573:]
1570:a
1567:[
1544:p
1533:(
1516:q
1493:q
1487:p
1464:p
1453:(
1433:p
1424:a
1412:p
1409:]
1406:a
1403:[
1364:0
1334:1
1308:0
1286:a
1255:a
1233:b
1211:a
1185:b
1180:;
1175:a
1153:b
1131:a
1109:b
1105:|
1101:a
1079:b
1076:+
1073:a
1047:b
1041:a
1019:b
997:a
920:p
914:]
911:a
908:[
899:p
893:a
868:p
859:a
847:p
844:]
841:a
838:[
812:p
790:a
768:p
746:a
724:p
718:a
693:p
671:a
649:p
627:a
605:p
602:]
599:a
596:[
567:a
542:]
539:a
536:[
514:a
492:p
472:p
447:p
427:p
359:]
356:P
353:[
276:P
247:a
227:b
221:a
201:b
197:;
193:a
183:p
179:a
165:p
159:a
146:p
142:a
128:p
125:]
122:a
119:[
85:,
77:]
69:[
20:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.