“modal logic”的概念、定义、翻译、参考文献-科学参考

modal logic

Computer

Any logical system that allows the use of modal operators designed to explore modes of truth. The two most common operators are ‘necessity’ and ‘possibility’, usually written as □ and ◊, where □F expresses ‘F is necessarily true’ and ◊F that ‘F is possibly true.’ The objective of modal logic is to pin down meanings and laws of reasoning for these modes of truth. Modal logic has been developed in philosophy and is now the basis of advanced technologies in computer science.
For a modal operator α‎, the value of a formula α‎F in an interpretation I depends on the values of F in a whole class of interpretations related to I, rather than on the value of F in just I itself as is the case in a nonmodal logic. Thus □F is true in an interpretation (or world) w if F is true in all worlds w′ related to (or accessible from) w, while ◊F is true in w if F is true in at least one such w′. In discussing the semantics of modal logic, therefore, one considers frames of the form (W,R), where W is a set of worlds and R is an accessibility relation on W. Each world attaches a value to all the primitive symbols in the language.
In dynamic logic the modal operators correspond to programs, and the worlds correspond to states of execution. Then the formula α‎F is true in a particular state s if F is true in all states reachable from s by running the program α‎. Dynamic logic is similar to Hoare logic in the fact that its formulas involve both programming and logical constructs.
In temporal logics the modal operators deal with interpretations that might depend on the time: formulas express ‘F is sometimes true’ or ‘F is always true’. Other modal operators express notions of belief, desirability, and obligation. All these ideas are of great relevance in reasoning about programs and systems. Hence recent years have seen extensive use of modal logics in program verification and formal specification, especially for concurrent programs and systems.

Logic

A modal logic is a logic which deals with the modalities of necessity and possibility. Such a logic was first formulated in Aristotle’s syllogistic and was investigated by medieval logicians. In its modern form, modal logic was developed by the logican Clarence Irving Lewis (1883–1964), who was motivated by the paradoxes of relevance. He produced five systems of logic, $S 1$ – $S 5$ . These were formulated purely axiomatically. Semantics for these logics were later developed by several people, but principally by Saul Kripke with Kripke semantics. It then became clear that Lewis’ systems were just five of an infinite number of such logics, and that the most basic of these, $K$ , was none of the Lewis systems.

Philosophy

A logic studying the notions of necessity and possibility. Modal logic was of great importance historically, particularly in the light of various doctrines concerning the necessary properties of the deity, but was not a central topic of modern logic in its golden period at the beginning of the 20th century. It was, however, revived by C. I. Lewis, by adding to a propositional or predicate calculus two operators, □ and ◊ (sometimes written N and M), meaning necessarily and possibly, respectively. Theses like p → ◊ p and □ p → p will be wanted. Controversial theses include □ p→ □□p (if a proposition is necessary, it is necessarily necessary, characteristic of the system known as S4) and ◊p→ □◊p (if a proposition is possible, it is necessarily possible, characteristic of the system known as S5). The classical model theory for modal logic, due to Kripke and the Swedish logician Stig Kanger, involves valuing propositions not as true or false simpliciter, but as true or false at possible worlds, with necessity then corresponding to truth in all worlds, and possibility to truth in some world. Various different systems of modal logic result from adjusting the accessibility relation between worlds. See Kripke model.

单词	modal logic
释义	modal logic Computer Any logical system that allows the use of modal operators designed to explore modes of truth. The two most common operators are ‘necessity’ and ‘possibility’, usually written as □ and ◊, where □F expresses ‘F is necessarily true’ and ◊F that ‘F is possibly true.’ The objective of modal logic is to pin down meanings and laws of reasoning for these modes of truth. Modal logic has been developed in philosophy and is now the basis of advanced technologies in computer science. For a modal operator α‎, the value of a formula α‎F in an interpretation I depends on the values of F in a whole class of interpretations related to I, rather than on the value of F in just I itself as is the case in a nonmodal logic. Thus □F is true in an interpretation (or world) w if F is true in all worlds w′ related to (or accessible from) w, while ◊F is true in w if F is true in at least one such w′. In discussing the semantics of modal logic, therefore, one considers frames of the form (W,R), where W is a set of worlds and R is an accessibility relation on W. Each world attaches a value to all the primitive symbols in the language. In dynamic logic the modal operators correspond to programs, and the worlds correspond to states of execution. Then the formula α‎F is true in a particular state s if F is true in all states reachable from s by running the program α‎. Dynamic logic is similar to Hoare logic in the fact that its formulas involve both programming and logical constructs. In temporal logics the modal operators deal with interpretations that might depend on the time: formulas express ‘F is sometimes true’ or ‘F is always true’. Other modal operators express notions of belief, desirability, and obligation. All these ideas are of great relevance in reasoning about programs and systems. Hence recent years have seen extensive use of modal logics in program verification and formal specification, especially for concurrent programs and systems. Logic A modal logic is a logic which deals with the modalities of necessity and possibility. Such a logic was first formulated in Aristotle’s syllogistic and was investigated by medieval logicians. In its modern form, modal logic was developed by the logican Clarence Irving Lewis (1883–1964), who was motivated by the paradoxes of relevance. He produced five systems of logic, $S 1$ – $S 5$ . These were formulated purely axiomatically. Semantics for these logics were later developed by several people, but principally by Saul Kripke with Kripke semantics. It then became clear that Lewis’ systems were just five of an infinite number of such logics, and that the most basic of these, $K$ , was none of the Lewis systems. Philosophy A logic studying the notions of necessity and possibility. Modal logic was of great importance historically, particularly in the light of various doctrines concerning the necessary properties of the deity, but was not a central topic of modern logic in its golden period at the beginning of the 20th century. It was, however, revived by C. I. Lewis, by adding to a propositional or predicate calculus two operators, □ and ◊ (sometimes written N and M), meaning necessarily and possibly, respectively. Theses like p → ◊ p and □ p → p will be wanted. Controversial theses include □ p→ □□p (if a proposition is necessary, it is necessarily necessary, characteristic of the system known as S4) and ◊p→ □◊p (if a proposition is possible, it is necessarily possible, characteristic of the system known as S5). The classical model theory for modal logic, due to Kripke and the Swedish logician Stig Kanger, involves valuing propositions not as true or false simpliciter, but as true or false at possible worlds, with necessity then corresponding to truth in all worlds, and possibility to truth in some world. Various different systems of modal logic result from adjusting the accessibility relation between worlds. See Kripke model.
随便看	Blake, Robert (1599–1657) Blakeslee, Albert Francis blanc fixe Blanc, Louis (1811–82) blancmange function Blanco, Antonio Guzmán Bland-Altman plot Blandford–Znajek process blank blank-and-burst blank character blanket bog blanketing blanking blanking level Blanqui, Louis Auguste (1805–81) -blast BLAST blast furnace blasting gelatin blasto- blastocoel blastocyst blastoderm blast-off