Veuillez choisir le dossier dans lequel vous souhaitez ajouter ce contenu :
Filtrer les résultats
Les premières tentatives d'application de la méthode des tables de vérité en logique temporelle remontent aux travaux d'A.N. Prior. S'appuyant sur l'interprétation doxastique des modalités, il a construit un algorithme (les matrices de Prior) qui n'était cependant décidable que pour des logiques comprenant un nombre restreint d'instants. La première partie de l'exposé consiste à présenter un algorithme qui permet de traiter une logique à une infinité d'instants tout en produisant un calcul fini. Cet algorithme s'appuie sur les types et les genres de tableaux de vérité élaborés dans le cadre de la science des genres et la méthode semi-décidable. La …