Discussion:Logique temporelle

Autres discussions [liste]

Admissibilité
Neutralité
Droit d'auteur
Article de qualité
Bon article
Lumière sur
À faire
Archives
Commons

Cet article est indexé par le projet Logique.

Les projets ont pour but d’enrichir le contenu de Wikipédia en aidant à la coordination du travail des contributeurs. Vous pouvez modifier directement cet article ou visiter les pages de projets pour prendre conseil ou consulter la liste des tâches et des objectifs.

**Évaluation** de l’article « **Logique temporelle** »
Avancement	Importance	pour le projet
Ébauche	Élevée		Logique (discussion • critères • liste • stats • hist. • comité • stats vues)

Cet article ne comporte pas de liste de tâches suggérées. Vous pouvez saisir une liste de tâches à accomplir (par exemple sous forme d'une liste à puces), puis sauvegarder. Vous pouvez aussi consulter la page d'aide.

Lien avec latch et clamp[modifier le code]

Je ne vois pas bien le lien avec latch et clamp (?)

Mononoke Hime 13 oct 2004 à 16:47 (CEST)

Je l'ai supprimé. Pierre de Lyon

Formulation de l'article[modifier le code]

Bonjour, je trouve vraiment que la sémantique proposée n'est pas claire, alors qu'on peut s'appuyer sur des sémantiques de Kripke pour les logiques temporelles les plus simples (avec un monde = un instant, même si dans d'autres logiques un monde = une demi-histoire). Est-ce que je suis le seul ? Je pense aussi que la description des modalités (notamment F et G) n'est pas bonne.

D'autre part, quid selon vous de l'intérêt d'articles séparés sur CTL et LTL (pour commencer), en plus d'un article sur les logiques temporelles en général ?

Question aux spécialistes (je n'ai pas mes bouquins sous la main, je suis en week-end), en LTL il n'y a pas de notion de passé, ni de modalités P ou H ?

Il y a plusieurs versions de la LTL, avec des opérateurs futurs (Always, Next, One-time, etc.) ou bien passés (Has-always-been, Previous, Once, etc.), voire les deux ! Voir par exemple ce lien [1] (je ne connais pas cet article, je suis tombé dessus en recherchant « LTL past operators » dans Google :-)

— ChrisJ 13 octobre 2007 à 20:05 (CEST)[répondre]

OK, donc c'est plus une famille de logiques. - Eusebius^[causons] 13 octobre 2007 à 20:12 (CEST)[répondre]

Je n'ai pas le temps de regarder le fond plus en détail, mais si tu jettes un coup d'œil à la version anglaise, tu verras qu'ils ont trouvé de la matière pour faire de longs articles sur la logique temporelle en général, la LTL, la CTL... — ChrisJ 13 octobre 2007 à 20:07 (CEST)[répondre]

Oui, c'était un peu l'idée. Mais je n'ai pas eu l'impression, pour avoir travaillé sur ces articles anglais aujourd'hui, que c'était vraiment le top du top. C'est pas grave, on fera mieux :-) - Eusebius^[causons] 13 octobre 2007 à 20:12 (CEST)[répondre]

Logique temporelle propositionnelle[modifier le code]

Ce qui est présentée dans l'article est la logique temporelle propositionnelle. Je pense qu'il faudrait le dire, car il y a une logique temporelle prédicative ou un calcul des prédicats temporel. Pierre de Lyon 15 novembre 2007 à 19:11 (CET)[répondre]

Comme après huit ans, ma question n'a pas été débattue, j'ai apporté une précision.--Pierre de Lyon (discuter) 28 septembre 2015 à 09:49 (CEST)[répondre]

Coquille?[modifier le code]

Les définitions de "until" et "release" m'ont l'air fausses quand on les compare à celles des pages des autres langues: avec ces définitions, on a: "pUq" = "qRp", il faudrait sans doute revoir les quantificateurs.

L'article anglais ne m'a pas l'air fameux, l'allemenand trop court et ne donne pas les définitions, mais l'article polonais m'a l'air bien (je ne parle pas le polonais, mais je devine la structure de l'article avec les formules). Sedrikov (d)

Effectivement (une relation correcte étant p U q ~ non(non(p) R non(q))) : corrigé dans le texte, mais pas dans l’image, ne sachant trop comment gérer les ressources de Commons ; j’ai cependant signalé une définition correcte en dessous de cette dernière, en attendant que quelqu’un utilise cette indication pour mettre à jour le fichier PNG. SniperMaské (discuter) 10 août 2016 à 20:51 (CEST)[répondre]

Pour un lecteur quidam[modifier le code]

Intérêt(s)[modifier le code]

Indiquer que les logiques arborescentes permettent d'aborder

les futurs possibles (futuribles, pilotage de crises, de négociations ; planifications diverses ; comportement de systèmes multi-opérateurs, multi-tâches etc... ) : les contradictions peuvent indiquer des futurs indésirables, et indiquer les décisions qui y mèneraient ;
les passés possibles (histoire, archéologie, enquêtes diverses), les contradictions indiquant les thèses incompatibles avec les faits, et de là les hypothèses irrecevables ;
peut-être en rapport avec les extensions au sens de McDermott ?

Distinguo[modifier le code]

Classifier en temps linéaire ou arborescent, discret ou continu, mais aussi temps borné ou non, en indiquant si possible quelques emplois correspondants à chaque cas

Sources de langue française[modifier le code]

je suggère "Approche logique de l'Intelligence Artificielle / A. Thayse et al., Dunod, 1988" --Lf69100 (discuter) 27 mai 2015 à 12:52 (CEST)[répondre]

Parle-t-on vraiment des logiques temporelles en général ?[modifier le code]

Bonjour,

en relisant l'article je m'aperçois qu'il parle plus de LTL en précisant plus loin que d'autres logiques temporelles existent. On ne trouve pas du tout le côté branchement de CTL* par exemple, l'explication semblant faire penser que le temps est toujours linéaire dans les logiques temporelles, ce qui est faux. Je pense qu'il faudrait déplacer la majorité de l'article dans LTL et écrire autre chose pour les logiques temporelles. (sinon une bonne référence pour les logiques temporelles est "Principle of model-checking")

--Tcharrie (discuter) 11 décembre 2015 à 15:08 (CET)[répondre]

Ca avait déjà signalé. N'hésite pas à faire les changements. --Pierre de Lyon (discuter) 12 décembre 2015 à 12:44 (CET)[répondre]