Dynamic Logic

By Silva, Andres | AI Magazine, Spring 2002 | Go to article overview

Dynamic Logic


Silva, Andres, AI Magazine


Harel, D.; Kozen, D.; and Tiuryn, J. Dynamic Logic. Cambridge, Massachusetts, The MIT Press, 2000, 459 pp., $50.00, ISBN 0-262-08289-6.

The real world is dynamic, and any intelligent perception of the world should include the concept of time. Remember that time and space are a priori conditions of human perception in Kant's philosophy. On the one hand, time is inherent to action and change; on the other, action and change are possible because of the passage of time. According to McDermott, "Dealing with time correctly would change everything in an Al program" (McDermott 1982, p. 101).

It should not be surprising then that temporal reasoning has always been a very important topic in many fields of Al, particularly areas dealing with change, causality, and action (planning, diagnosis, natural language understanding, and so on). Al developments based on temporal reasoning lead to general theories about time and action, such as McDermott's (1982) temporal logic, Vilain's (1982) theory of time, and Allen's (1984) theory of action and time. Work on the application of these results has taken place in fields such as planning and medical knowledge-based systems.

However, action and change are not an exclusive interest of AI. In mainstream computer science, any execution of a "traditional" computer program is considered to perform an action that leads to a change of state.

From this point of view, the field of program verification, traditionally focused on the correctness of actions carried out by program executions, can potentially provide AI with many approaches suitable for dealing with action and change. Temporal logic and dynamic logic are two of the approaches that have been used in the fields of both Al and program verification, temporal logic being the most popular. Both temporal and dynamic logic provide alternative applications of modal logic to program specification and verification. The main difference between the two is that temporal logic is endogenous, and dynamic logic is exogenous. A logic is exogenous if programs (actions) are explicit in the language. Temporal logic is endogenous, so its programs (actions) are never explicit in the language. Dynamic logic subsumes temporal logic.

Some cross-fertilization has already take place between AI, temporal logic, and dynamic logic. I focus on dynamic logic, which is the topic that is covered at length in the book under review. Dynamic logic is an approach to program verification with strong Al potential. One of the most prominent uses of dynamic logic in Al was Moore's (1990) approach. Moore formalized some issues related to agency, with a focus on what an agent needs to know to be able to perform an action. For more information on this topic and a clear demonstration of the usefulness of dynamic logic for agent reasoning and action, see the survey by Meyer (1999). Also, some research in knowledge engineering inspired by, or making use of, dynamic logic has been published van Harmelen and Balder (1992) and Fensel (1995).

Dynamic logic is an eclectic approach to program verification, as is evidenced by its history. This history starts with the pragmatics of programming, that is, the study of the actions that programs perform and the correctness of these actions. This has been a major issue in computer science since Dijkstra's (1968) attacks on the GOTO statement. Perhaps the most popular formal approach aimed at proving program correctness is Hoare's (1969), which is based on correctness assertions. In Hoare's logic, statements of the form (aP(b say that if program P starts in an input state satisfying a, then if and when P halts, it does so in a state satisfying b. Hoare provided some inference rules used to infer assertions about programs from assertions about other programs. IMAGE FORMULA16IMAGE FORMULA17

Here we have a book that provides a deep insight into the topic of dynamic logic. …

The rest of this article is only available to active members of Questia

Already a member? Log in now.

Notes for this article

Add a new note
If you are trying to select text to create highlights or citations, remember that you must now click or tap on the first word, and then click or tap on the last word.
One moment ...
Default project is now your active project.
Project items

Items saved from this article

This article has been saved
Highlights (0)
Some of your highlights are legacy items.

Highlights saved before July 30, 2012 will not be displayed on their respective source pages.

You can easily re-create the highlights by opening the book page or article, selecting the text, and clicking “Highlight.”

Citations (0)
Some of your citations are legacy items.

Any citation created before July 30, 2012 will labeled as a “Cited page.” New citations will be saved as cited passages, pages or articles.

We also added the ability to view new citations from your projects or the book or article where you created them.

Notes (0)
Bookmarks (0)

You have no saved items from this article

Project items include:
  • Saved book/article
  • Highlights
  • Quotes/citations
  • Notes
  • Bookmarks
Notes
Cite this article

Cited article

Style
Citations are available only to our active members.
Buy instant access to cite pages or passages in MLA, APA and Chicago citation styles.

(Einhorn, 1992, p. 25)

(Einhorn 25)

1. Lois J. Einhorn, Abraham Lincoln, the Orator: Penetrating the Lincoln Legend (Westport, CT: Greenwood Press, 1992), 25, http://www.questia.com/read/27419298.

Cited article

Dynamic Logic
Settings

Settings

Typeface
Text size Smaller Larger Reset View mode
Search within

Search within this article

Look up

Look up a word

  • Dictionary
  • Thesaurus
Please submit a word or phrase above.
Print this page

Print this page

Why can't I print more than one page at a time?

Help
Full screen

matching results for page

    Questia reader help

    How to highlight and cite specific passages

    1. Click or tap the first word you want to select.
    2. Click or tap the last word you want to select, and you’ll see everything in between get selected.
    3. You’ll then get a menu of options like creating a highlight or a citation from that passage of text.

    OK, got it!

    Cited passage

    Style
    Citations are available only to our active members.
    Buy instant access to cite pages or passages in MLA, APA and Chicago citation styles.

    "Portraying himself as an honest, ordinary person helped Lincoln identify with his audiences." (Einhorn, 1992, p. 25).

    "Portraying himself as an honest, ordinary person helped Lincoln identify with his audiences." (Einhorn 25)

    "Portraying himself as an honest, ordinary person helped Lincoln identify with his audiences."1

    1. Lois J. Einhorn, Abraham Lincoln, the Orator: Penetrating the Lincoln Legend (Westport, CT: Greenwood Press, 1992), 25, http://www.questia.com/read/27419298.

    Cited passage

    Thanks for trying Questia!

    Please continue trying out our research tools, but please note, full functionality is available only to our active members.

    Your work will be lost once you leave this Web page.

    Buy instant access to save your work.

    Already a member? Log in now.

    Oops!

    An unknown error has occurred. Please click the button below to reload the page. If the problem persists, please try again in a little while.