| dbpprop:abstract
|
- In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a particular modal logic-based system of temporal logic introduced by Arthur Prior in the 1960s. Subsequently it has been developed further by computer scientists, notably Amir Pnueli, and logicians. Temporal logic was first studied in depth by Aristotle, whose writings are filled with an early, partially-developed form of first-order temporal modal binary logic. Any logic which uses the existential quantifier or the universal quantifier is said to be a predicate logic. Any logic which views time as a sequence of states is a temporal logic, and any logic which uses only two truth values is a binary logic. Consider the statement: "I am hungry. " Though its meaning is constant in time, the truth value of the statement can vary in time. Sometimes the statement is true, and sometimes the statement is false, but the statement is never true and false simultaneously. In a temporal logic, statements can have a truth value which can vary in time. Contrast this with an atemporal logic, which can only discuss statements whose truth value is constant in time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry until I eat something". Temporal logic has found an important application in formal verification, where it is used to state requirements of hardware or software systems. For instance, one may wish to say that whenever a request is made, access to a resource is eventually granted, but it is never granted to two requestors simultaneously. " Such a statement can conveniently be expressed in a temporal logic. Temporal logic always has the ability to reason about a time line. So called linear time logics are restricted to this type of reasoning. Branching logics, however, can reason about multiple time lines. This presupposes an environment that may act unpredictably. To continue the example, in a branching logic we may state that "there is a possibility that I will stay hungry forever. " We may also state that "there is a possibility that eventually I am no longer hungry. " If we do not know whether or not I will ever get fed, these statements are both true. Two early contenders in formal verifications were Linear Temporal Logic (a linear time logic by Amir Pnueli and Zohar Manna) and Computation Tree Logic, a branching time logic by Edmund Clarke and E. Allen Emerson. The fact that the second logic is more efficient than the first does not reflect on branching and linear logics in general, as has sometimes been argued. Rather, Emerson and Lei show that any linear logic can be extended to a branching logic that can be decided with the same complexity.
- Die Temporale Logik ist eine Erweiterung der Logik, so dass zeitliche Abläufe erfasst werden können. Dabei wird keine kontinuierliche Zeit betrachtet, sondern nur eine Art Vorher/Nachher-Beziehung. Die beiden wichtigsten Temporalen Logiken sind die Lineare temporale Logik (LTL) und Computation Tree Logic (CTL). Während LTL von einer linearen Abfolge von Zeitpunkten ausgeht beschreibt CTL ein verzweigende Zeitfolge. Weil beide Logiken verschiede Sachverhalte beschreiben können, aber auch eine große Schnittmenge haben, definiert man CTL* von welchen sowohl CTL, wie auch LTL, eine Teilmenge sind.
- La lógica temporal es un tipo de lógica modal usada para describir un sistema de reglas y simbolismos para la representación y el razonamiento sobre proposiciones en las que tiene presencia el factor tiempo. Existe una cierta relación con otras variedades de lógica, por ejemplo, la lógica modal. Su estudio tiene una cierta importancia dentro del estudio de la informática, en particular los desarrollos introducidos por Amir Pnueli. Por ejemplo, tomemos la sentencia: "Tengo hambre"; aunque su significado es independiente del tiempo, el valor de verdad o falsedad de la misma puede variar con el tiempo en un determinado sistema que incluya acciones de comer; así, en función del sistema, algunas veces será cierta y otras falsa, aunque nunca será cierta y falsa simultáneamente.
- Temporaalilogiikka eli temporaalinen logiikka on modaalilogiikan alue, joka käsittelee aikaan liittyvää päättelyä ja käsitteitä. Temporaalilogiikan esitteli Arthur Prior 1960-luvulla. Sen jälkeen sitä ovat kehittäneet sekä tietojenkäsittelytieteilijät, erityisesti Amir Pnueli, että loogikot. Temporaalilogiikoihin kuuluvat CTL*, intervallitemporaalilogiikka (ITL) ja μ-kalkyyli.
- Les différentes logiques temporelles sont des logiques mathématiques et plus précisément des logiques modales. Intuitivement, cela signifie que la notion de vérité dans ces logiques dépend de l'évolution du monde. C'est-à-dire qu'une proposition peut-être, à un moment, fausse puis, plus tard, devenir vrai, etc.
- 時相論理(Temporal Logic)とは、時間との関連で問題を理解し表現するための規則と表記法の体系である。1960年代に Arthur Prior が提唱した様相論理学に基づいた時相論理を特に時制論理(Tense Logic)と呼ぶことがある。その後、そこから発展し、アミール・プヌーリら計算機科学者や論理学者が研究を進めた。
- Tijdslogica's of temporele logica's kunnen worden gezien als uitbreiding van de propositielogica, de predicatenlogica, de modale logica of de hybride logica. Hierbij is er extra formele apparatuur om uit te drukken of iets in het verleden, het heden, de toekomst het geval is, mogelijk het geval is, of het in een mogelijke toekomst het geval is, enzovoorts. Met andere woorden kan temporele informatie met het formele systeem verwerkt worden. Een van de onderscheiden die bij temporele logica's worden gemaakt, is die tussen logica's die tijd als een lineair gegeven zien, en die die het toestaan, dat er vertakkingen in de tijd bestaan. Dit laatste kan gezien worden als mogelijke toekomstige scenario's, of, bijvoorbeeld in een sciencefiction setting of de kwantummechanica, toekomstige parallelle werelden binnen een multiversum. Een ander onderscheid is dat tussen systemen die tijd discreet beschouwen, zoals als verzameling tijdstippen, en die waarbij tijd continu is. Voorbeelden van tijdslogica's zijn die van Arthur Prior en die van Hans Reichenbach.
- Logika temporalna – logika umożliwiająca rozważanie zależności czasowych bez wprowadzania czasu explicite. Pierwotnie służyła jako narzędzie do filozoficznych rozważań nad naturą czasu, dzisiaj jest używana głównie w informatyce. Czas można wprowadzić do zwykłego rachunku predykatów pierwszego rzędu. Np. żeby powiedzieć, że zawsze kiedy jedzie pociąg szlaban musi być opuszczony (żeby uniknąć wypadku), oraz że dla każdej chwili czasu szlaban kiedyś się podniesie (żeby samochody mogły w końcu przejechać), możemy napisać: <math>\forall t. \;\mbox{pociag jedzie}(t) \rightarrow \neg \mbox{szlaban podniesiony}(t)</math> <math>\forall t. \;\exists t^\prime > t . \; \mbox{szlaban podniesiony}(t^\prime)</math> Dowodzenie twierdzeń w tak ogólnej notacji może być jednak trudne. Z tego powodu dodaje się do rachunku zdań, bez kwantyfikatorów, pewne operatory modalne. Brak kwantyfikatorów umożliwia nam łatwe dowodzenie twierdzeń, zaś operatory modalne umożliwiają nam rozważanie zależności czasowych. Logik temporalnych jest wiele, można je jednak podzielić na dwie grupy – te, które zakładają liniową strukturę czasu, oraz te, które zakładają rozgałęzioną strukturę czasu. Logiki temporalne zazwyczaj operują na czasie składającym się z dyskretnych wydarzeń, choć możliwe są też logiki używające czasu ciągłego.
- Темпоральная логика в логике — это логика, учитывающая причинно-следственные связи в условиях времени. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале. Она была разработана в 1960-х Артуром Приором на основе модальной логики и получила дальнейшее развитие в информатике благодаря трудам лауреата Тьюринговской премии Амира Пнуэли. Есть два подхода темпоральной логики, основанные на принципах здравого смысла и диалектики: «после этого» означает «по причине этого», либо «после этого» означает «позже» в хронологическом смысле.
- 在逻辑中,术语时间逻辑被用来描述为表现和推理关于时间限定的命题的规则和符号化的任何系统。它有时也被称为时态逻辑,这是 Arthur Prior 在1960年代介入的基于模态逻辑的特殊的时间逻辑系统。它后来被计算机科学家特别是 Amir Pnueli 和逻辑学家进一步的开发。 时间逻辑首先被亚里士多德深入研究过,他的著作中有粗糙形式的一阶时间模态二值逻辑。使用存在量词或全称量词的任何逻辑都叫做一阶逻辑。把时间看作状态的序列的任何逻辑都是时间逻辑,只使用两个真值的任何逻辑都是二值逻辑。 考虑陈述:"我饿了"。尽管它的意思随时间恒定,但这个陈述的真值随时间可变。有时这个陈述为真,有时这个陈述为假,但是这个陈述不能同时为真并且为假。在时间逻辑中,陈述可以有随时间变化的真值。与之相对的是非时间逻辑,它只能处理有着随时间恒定的真值的陈述。 三个基本时间算子是:总是、有时、和永不。 计算树逻辑(CTL)、线性时间逻辑(LTL)和间隔时间逻辑(ITL)是时间逻辑的例子。
|
| rdfs:comment
|
- In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a particular modal logic-based system of temporal logic introduced by Arthur Prior in the 1960s. Subsequently it has been developed further by computer scientists, notably Amir Pnueli, and logicians.
- Die Temporale Logik ist eine Erweiterung der Logik, so dass zeitliche Abläufe erfasst werden können. Dabei wird keine kontinuierliche Zeit betrachtet, sondern nur eine Art Vorher/Nachher-Beziehung. Die beiden wichtigsten Temporalen Logiken sind die Lineare temporale Logik (LTL) und Computation Tree Logic (CTL). Während LTL von einer linearen Abfolge von Zeitpunkten ausgeht beschreibt CTL ein verzweigende Zeitfolge.
- La lógica temporal es un tipo de lógica modal usada para describir un sistema de reglas y simbolismos para la representación y el razonamiento sobre proposiciones en las que tiene presencia el factor tiempo. Existe una cierta relación con otras variedades de lógica, por ejemplo, la lógica modal. Su estudio tiene una cierta importancia dentro del estudio de la informática, en particular los desarrollos introducidos por Amir Pnueli.
- Temporaalilogiikka eli temporaalinen logiikka on modaalilogiikan alue, joka käsittelee aikaan liittyvää päättelyä ja käsitteitä. Temporaalilogiikan esitteli Arthur Prior 1960-luvulla. Sen jälkeen sitä ovat kehittäneet sekä tietojenkäsittelytieteilijät, erityisesti Amir Pnueli, että loogikot. Temporaalilogiikoihin kuuluvat CTL*, intervallitemporaalilogiikka (ITL) ja μ-kalkyyli.
- Les différentes logiques temporelles sont des logiques mathématiques et plus précisément des logiques modales. Intuitivement, cela signifie que la notion de vérité dans ces logiques dépend de l'évolution du monde. C'est-à-dire qu'une proposition peut-être, à un moment, fausse puis, plus tard, devenir vrai, etc.
- 時相論理(Temporal Logic)とは、時間との関連で問題を理解し表現するための規則と表記法の体系である。1960年代に Arthur Prior が提唱した様相論理学に基づいた時相論理を特に時制論理(Tense Logic)と呼ぶことがある。その後、そこから発展し、アミール・プヌーリら計算機科学者や論理学者が研究を進めた。
- Tijdslogica's of temporele logica's kunnen worden gezien als uitbreiding van de propositielogica, de predicatenlogica, de modale logica of de hybride logica. Hierbij is er extra formele apparatuur om uit te drukken of iets in het verleden, het heden, de toekomst het geval is, mogelijk het geval is, of het in een mogelijke toekomst het geval is, enzovoorts. Met andere woorden kan temporele informatie met het formele systeem verwerkt worden.
- Logika temporalna – logika umożliwiająca rozważanie zależności czasowych bez wprowadzania czasu explicite. Pierwotnie służyła jako narzędzie do filozoficznych rozważań nad naturą czasu, dzisiaj jest używana głównie w informatyce. Czas można wprowadzić do zwykłego rachunku predykatów pierwszego rzędu. Np.
- Темпоральная логика в логике — это логика, учитывающая причинно-следственные связи в условиях времени. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале.
|