In
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
,
philosophy
Philosophy (from , ) is the systematized study of general and fundamental questions, such as those about existence, reason, knowledge, values, mind, and language. Such questions are often posed as problems to be studied or resolved. Some ...
, and
theoretical computer science
Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory.
It is difficult to circumsc ...
, dynamic logic is an extension of
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
capable of encoding properties of
computer program
A computer program is a sequence or set of instructions in a programming language for a computer to execute. Computer programs are one component of software, which also includes documentation and other intangible components.
A computer program ...
s.
A simple example of a statement in dynamic logic is
:
which states that if the ground is currently dry and it rains, then afterwards the ground will be wet.
The syntax of dynamic logic contains a language of ''propositions'' (like "the ground is dry") and a language of ''actions'' (like "it rains"). The core modal constructs are
, which states that after performing action ''a'' the proposition ''p'' should hold, and
, which states that after performing action ''a'' it is possible that ''p'' holds.
The action language supports operations
(doing one action followed by another),
(doing one action or another), and iteration
(doing one action zero or more times). The proposition language supports
Boolean operations (and, or, and not). The action logic is expressive enough to encode programs. For an arbitrary program
,
precondition
In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification.
If a precondition is violated, the effect of the s ...
, and
postcondition In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions wit ...
, the dynamic logic statement
encodes the correctness of the program, making dynamic logic more general than
Hoare logic
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and log ...
.
Beyond its use in
formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
of programs, dynamic logic has been applied to describe complex behaviors arising in
linguistics
Linguistics is the scientific study of human language. It is called a scientific study because it entails a comprehensive, systematic, objective, and precise analysis of all aspects of language, particularly its nature and structure. Linguis ...
,
philosophy
Philosophy (from , ) is the systematized study of general and fundamental questions, such as those about existence, reason, knowledge, values, mind, and language. Such questions are often posed as problems to be studied or resolved. Some ...
,
AI, and other fields.
Language
Modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
is characterized by the
modal operator
A modal connective (or modal operator) is a logical connective for modal logic. It is an operator which forms propositions from propositions. In general, a modal operator has the "formal" property of being non-truth-functional in the following sen ...
s
(box p) asserting that
is necessarily the case, and
(diamond p) asserting that
is possibly the case. Dynamic logic extends this by associating to every action
the modal operators
and
, thereby making it a
multimodal logic A multimodal logic is a modal logic that has more than one primitive modal operator. They find substantial applications in theoretical computer science.
Overview
A modal logic with ''n'' primitive unary modal operators \Box_i, i\in \ is called an ...
. The meaning of
is that after performing action
it is necessarily the case that
holds, that is,
must bring about
. The meaning of
is that after performing
it is possible that
holds, that is,
might bring about
. These operators
dual to each other, which means they are related by
and
, analogously to the relationship between the universal (
) and existential (
) quantifiers.
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,
Kleene
Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
's
regular expression
A regular expression (shortened as regex or regexp; sometimes referred to as rational expression) is a sequence of characters that specifies a search pattern in text. Usually such patterns are used by string-searching algorithms for "find" or ...
operators are a good match to modal logic. Given actions
and
, the compound action
, ''choice'', also written
or
, is performed by performing one of
or
. The compound action
, ''sequence'', is performed by performing first
and then
. The compound action
, ''iteration'', is performed by performing
zero or more times, sequentially. The constant action
or BLOCK does nothing and does not terminate, whereas the constant action
or SKIP or NOP, definable as
, does nothing but does terminate.
Axioms
These operators can be axiomatized in dynamic logic as follows, taking as already given a suitable axiomatization of
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
including such axioms for modal operators as the above-mentioned axiom
and the two inference rules ''
modus ponens
In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. ...
'' (
and
implies
) and ''necessitation'' (
implies
).
A1.
A2.
A3.
A4.
A5.
A6.
Axiom A1 makes the empty promise that when BLOCK terminates,
will hold, even if
is the proposition false. (Thus BLOCK abstracts the essence of the action of hell freezing over.)
A2 says that NOP acts as the identity function on propositions, that is, it transforms
into itself.
A3 says that if doing one of
or
must bring about
, then
must bring about
and likewise for
, and conversely.
A4 says that if doing
and then
must bring about
, then
must bring about a situation in which
must bring about
.
A5 is the evident result of applying A2, A3 and A4 to the equation
of
Kleene algebra
In mathematics, a Kleene algebra ( ; named after Stephen Cole Kleene) is an idempotent (and thus partially ordered) semiring endowed with a closure operator. It generalizes the operations known from regular expressions.
Definition
Various ine ...
.
A6 asserts that if
holds now, and no matter how often we perform
it remains the case that the truth of
after that performance entails its truth after one more performance of
, then
must remain true no matter how often we perform
. A6 is recognizable as
mathematical induction
Mathematical induction is a method for proving that a statement ''P''(''n'') is true for every natural number ''n'', that is, that the infinitely many cases ''P''(0), ''P''(1), ''P''(2), ''P''(3), ... all hold. Informal metaphors help ...
with the action n := n+1 of incrementing n generalized to arbitrary actions
.
Derivations
The modal logic axiom
permits the derivation of the following six theorems corresponding to the above:
T1.
T2.
T3.
T4.
T5.
T6.
T1 asserts the impossibility of bringing anything about by performing BLOCK.
T2 notes again that NOP changes nothing, bearing in mind that NOP is both deterministic and terminating whence
and
have the same force.
T3 says that if the choice of
or
could bring about
, then either
or
alone could bring about
.
T4 is just like A4.
T5 is explained as for A5.
T6 asserts that if it is possible to bring about
by performing
sufficiently often, then either
is true now or it is possible to perform
repeatedly to bring about a situation where
is (still) false but one more performance of
could bring about
.
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.
The difference between implication and inference is the same in dynamic logic as in any other logic: whereas the implication
asserts that if
is true then so is
, the inference
asserts that if
is valid then so is
. 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
, for example, is sound because its premise asserts that
holds at all times, whence no matter where
might take us,
will be true there. The implication
is not valid, however, because the truth of
at the present moment is no guarantee of its truth after performing
. For example,
will be true in any situation where
is false, or in any situation where
is true, but the assertion
is false in any situation where
has value 1, and therefore is not valid.
Derived rules of inference
As for modal logic, the inference rules ''modus ponens'' and ''necessitation'' 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 it, then repeatedly kicking it can't possibly fix it either. Writing
for the action of kicking the TV, and
for the proposition that the TV is broken, dynamic logic expresses this inference as
, having as premise
and as conclusion
. The meaning of
is that it is guaranteed that after kicking the TV, it is broken. Hence the premise
means that if the TV is broken, then after kicking it once it will still be broken.
denotes the action of kicking the TV zero or more times. Hence the conclusion
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.
The inference
is sound. However the implication
is not valid because we can easily find situations in which
holds but
does not. In any such counterexample situation,
must hold but
must be false, while
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
hold now, whereas the inference succeeds (is sound) because it requires that
hold in all situations, not just the present one.
An example of a valid implication is the proposition
. This says that if
is greater or equal to 3, then after incrementing
,
must be greater or equal to 4. In the case of deterministic actions
that are guaranteed to terminate, such as
, ''must'' and ''might'' have the same force, that is,
and
have the same meaning. Hence the above proposition is equivalent to
asserting that if
is greater or equal to 3 then after performing
,
might be greater or equal to 4.
Assignment
The general form of an assignment statement is
where
is a variable and
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.
A7.
This is a schema in the sense that
can be instantiated with any formula
containing zero or more instances of a variable
. The meaning of
is
with those occurrences of
that occur free in
, i.e. not bound by some quantifier as in
, replaced by
. For example, we may instantiate A7 with
, or with
. Such an axiom schema allows infinitely many axioms having a common form to be written as a finite expression connoting that form.
The instance
of A7 allows us to calculate mechanically that the example
encountered a few paragraphs ago is equivalent to
, which in turn is equivalent to
by
elementary algebra
Elementary algebra encompasses the basic concepts of algebra. It is often contrasted with arithmetic: arithmetic deals with specified numbers, whilst algebra introduces variables (quantities without fixed values).
This use of variables entai ...
.
An example illustrating assignment in combination with
is the proposition
. This asserts that it is possible, by incrementing
sufficiently often, to make
equal to 7. This of course is not always true, e.g. if
is 8 to begin with, or 6.5, whence this proposition is not a theorem of dynamic logic. If
is of type integer however, then this proposition is true if and only if
is at most 7 to begin with, that is, it is just a roundabout way of saying
.
Mathematical induction
Mathematical induction is a method for proving that a statement ''P''(''n'') is true for every natural number ''n'', that is, that the infinitely many cases ''P''(0), ''P''(1), ''P''(2), ''P''(3), ... all hold. Informal metaphors help ...
can be obtained as the instance of A6 in which the proposition
is instantiated as
, the action
as
, and
as
. The first two of these three instantiations are straightforward, converting A6 to
. However, the ostensibly simple substitution of
for
is not so simple as it brings out the so-called ''referential opacity'' of modal logic in the case when a modality can interfere with a substitution.
When we substituted
for
, we were thinking of the proposition symbol
as a
rigid designator
In modal logic and the philosophy of language, a term is said to be a rigid designator or absolute substantial term when it designates (picks out, denotes, refers to) the same thing in ''all possible worlds'' in which that thing exists. A designato ...
with respect to the modality
, meaning that it is the same proposition after incrementing
as before, even though incrementing
may impact its truth. Likewise, the action
is still the same action after incrementing
, even though incrementing
will result in its executing in a different environment. However,
itself is not a rigid designator with respect to the modality
; if it denotes 3 before incrementing
, it denotes 4 after. So we can't just substitute
for
everywhere in A6.
One way of dealing with the opacity of modalities is to eliminate them. To this end, expand
as the infinite conjunction
, that is, the conjunction over all
of
. Now apply A4 to turn
into
, having
modalities. Then apply Hoare's axiom
times to this to produce
, then simplify this infinite conjunction to
. This whole reduction should be applied to both instances of
in A6, yielding
. The remaining modality can now be eliminated with one more use of Hoare's axiom to give
.
With the opaque modalities now out of the way, we can safely substitute
for
in the usual manner of
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
to obtain
Peano
Giuseppe Peano (; ; 27 August 1858 – 20 April 1932) was an Italian mathematician and glottologist. The author of over 200 books and papers, he was a founder of mathematical logic and set theory, to which he contributed much notation. The stand ...
's celebrated axiom
, namely mathematical induction.
One subtlety we glossed over here is that
should be understood as ranging over the natural numbers, where
is the superscript in the expansion of
as the union of
over all natural numbers
. The importance of keeping this typing information straight becomes apparent if
had been of type ''integer'', or even ''real'', for any of which A6 is perfectly valid as an axiom. As a case in point, if
is a real variable and
is the predicate
''is a natural number'', then axiom A6 after the first two substitutions, that is,
, is just as valid, that is, true in every state regardless of the value of
in that state, as when
is of type ''natural number''. If in a given state
is a natural number, then the antecedent of the main implication of A6 holds, but then
is also a natural number so the consequent also holds. If
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
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 ''must'' be false.
Test
Dynamic logic associates to every proposition
an action
called a test. When
holds, the test
acts as a NOP, changing nothing while allowing the action to move on. When
is false,
acts as BLOCK. Tests can be axiomatized as follows.
A8.
The corresponding theorem for
is:
T8.
The construct if p then a else b is realized in dynamic logic as
. This action expresses a guarded choice: if
holds then
is equivalent to
, whereas
is equivalent to BLOCK, and
is equivalent to
. Hence when
is true the performer of the action can only take the left branch, and when
is false the right.
The construct while p do a is realized as
. This performs
zero or more times and then performs
. As long as
remains true, the
at the end blocks the performer from terminating the iteration prematurely, but as soon as it becomes false, further iterations of the body
are blocked and the performer then has no choice but to exit via the test
.
Quantification as random assignment
The random-assignment statement
denotes the nondeterministic action of setting
to an arbitrary value.
then says that
holds no matter what you set
to, while
says that it is possible to set
to a value that makes
true.
thus has the same meaning as the universal quantifier
, while
similarly corresponds to the existential quantifier
. That is, first-order logic can be understood as the dynamic logic of programs of the form
.
Dijkstra claimed to show the impossibility of a program that sets the value of variable
to an arbitrary positive integer.
However, in dynamic logic with assignment and the * operator,
can be set to an arbitrary positive integer with the dynamic logic program
. Hence we must either reject Dijkstra's argument or hold that the * operator is not effective.
Possible-world semantics
Modal logic is most commonly interpreted in terms of
possible world
A possible world is a complete and consistent way the world is or could have been. Possible worlds are widely used as a formal device in logic, philosophy, and linguistics in order to provide a semantics for intensional logic, intensional and mod ...
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 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
systems of logic
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...
including dynamic logic.
Propositional dynamic logic (PDL)
Ordinary or
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
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
contains all three types:
,
, and
are data,
is an action, and
and
are assertions.
Propositional logic
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
is derived from first-order logic by omitting data terms and reasons only about abstract propositions, which may be simple
propositional variable
In mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is an input variable (that can either be true or false) of a truth function. Propositional variables are the basic building-blocks of propositi ...
s or atoms or compound propositions built with such logical connectives as ''and'', ''or'', and ''not''.
Propositional dynamic logic, or PDL, was derived from dynamic logic in 1977 by
Michael J. Fischer and
Richard Ladner. 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
is in first-order dynamic logic. PDL is to (first-order) dynamic logic as propositional logic is to first-order logic.
Fischer and Ladner showed in their 1977 paper that PDL satisfiability was of
computational complexity
In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations) ...
at most
nondeterministic exponential time, and at least
deterministic exponential time in the worst case. This gap was closed in 1978 by
Vaughan Pratt
Vaughan Pratt (born April 12, 1944) is a Professor Emeritus at Stanford University, who was an early pioneer in the field of computer science. Since 1969, Pratt has made several contributions to foundational areas such as search algorithms, sorti ...
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
Gabbay (unpublished note),
Parikh
Parikh is a name found among Hindus of the Bania caste and also Jains. In means ''assayer'' in the Gujarati language and has its roots in the Sanskrit word for ''examiner''. Both the Oswal and Porwal communities of India have clans called ''Parek ...
(1978), Pratt (1979), and
Kozen and Parikh (1981).
History
Dynamic logic was developed by
Vaughan Pratt
Vaughan Pratt (born April 12, 1944) is a Professor Emeritus at Stanford University, who was an early pioneer in the field of computer science. Since 1969, Pratt has made several contributions to foundational areas such as search algorithms, sorti ...
in 1974 in notes for a class on program verification as an approach to assigning meaning to
Hoare logic
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and log ...
by expressing the Hoare formula
as
. The approach was later published in 1976 as a
logical system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...
in its own right. The system parallels
Andrzej Salwicki's system of
algorithmic logic and
Edsger Dijkstra
Edsger Wybe Dijkstra ( ; ; 11 May 1930 – 6 August 2002) was a Dutch computer scientist, programmer, software engineer, systems scientist, and science essayist. He received the 1972 Turing Award for fundamental contributions to developing progra ...
's notion of weakest-precondition predicate transformer
, with
corresponding to Dijkstra's
, 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
predicate transformers 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.
The concurrency challenge
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 sequential case. In contrast
Amir Pnueli
Amir Pnueli ( he, אמיר פנואלי; April 22, 1941 – November 2, 2009) was an Israeli computer scientist and the 1996 Turing Award recipient.
Biography
Pnueli was born in Nahalal, in the British Mandate of Palestine (now in Israel) and rec ...
's 1977 system of
temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
, 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,
deadlock
In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a lo ...
,
livelock
In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a loc ...
, fairness, etc.
See also
*
Hoare logic
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and log ...
*
Kleene algebra
In mathematics, a Kleene algebra ( ; named after Stephen Cole Kleene) is an idempotent (and thus partially ordered) semiring endowed with a closure operator. It generalizes the operations known from regular expressions.
Definition
Various ine ...
*
Temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
*
Temporal logic in finite-state verification
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
*
Temporal logic of actions
Temporal logic of actions (TLA) is a logic developed by Leslie Lamport, which combines temporal logic with a logic of actions.
It is used to describe behaviours of concurrent and distributed systems. It is the logic underlying the specification l ...
*
Modal μ-calculus In theoretical computer science, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding the least fixed point opera ...
Further reading
*
David Harel
David Harel ( he, דוד הראל; born 12 April 1950) is a computer scientist, currently serving as President of the Israel Academy of Sciences and Humanities. He has been on the faculty of the Weizmann Institute of Science in Israel since 1980, ...
,
Dexter Kozen
Dexter Campbell Kozen (born December 20, 1951) is an American theoretical computer scientist. He is Joseph Newton Pew, Jr. Professor in Engineering at Cornell University. He received his B.A. from Dartmouth College in 1974 and his PhD in compute ...
, and Jerzy Tiuryn, "Dynamic Logic". MIT Press, 2000 (450 pp).
* Nicolas Troquard and Philippe Balbiani
"Propositional Dynamic Logic."Stanford encyclopedia of philosophy
The ''Stanford Encyclopedia of Philosophy'' (''SEP'') combines an online encyclopedia of philosophy with peer-reviewed publication of original papers in philosophy, freely accessible to Internet users. It is maintained by Stanford University. Eac ...
, 2007.
Footnotes
{{reflist
References
*
Vaughan Pratt
Vaughan Pratt (born April 12, 1944) is a Professor Emeritus at Stanford University, who was an early pioneer in the field of computer science. Since 1969, Pratt has made several contributions to foundational areas such as search algorithms, sorti ...
, "Semantical Considerations on Floyd-Hoare Logic", Proc. 17th Annual IEEE
Symposium on Foundations of Computer Science
The IEEE Annual Symposium on Foundations of Computer Science (FOCS) is an academic conference in the field of theoretical computer science. FOCS is sponsored by the IEEE Computer Society.
As writes, FOCS and its annual Association for Computing ...
, 1976, 109-121.
*
David Harel
David Harel ( he, דוד הראל; born 12 April 1950) is a computer scientist, currently serving as President of the Israel Academy of Sciences and Humanities. He has been on the faculty of the Weizmann Institute of Science in Israel since 1980, ...
, "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.
*
David Harel
David Harel ( he, דוד הראל; born 12 April 1950) is a computer scientist, currently serving as President of the Israel Academy of Sciences and Humanities. He has been on the faculty of the Weizmann Institute of Science in Israel since 1980, ...
,
Dexter Kozen
Dexter Campbell Kozen (born December 20, 1951) is an American theoretical computer scientist. He is Joseph Newton Pew, Jr. Professor in Engineering at Cornell University. He received his B.A. from Dartmouth College in 1974 and his PhD in compute ...
, 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.
External links
Semantical Considerations on Floyd-Hoare Logic(original paper on dynamic logic)
Chapter 6 : Logic and Actionat ''Logic In Action'' site
Lecture Notes on Dynamic Logicby André Platzer
Modal logic
Logic in computer science
Non-classical logic