Titre original :
Deductive Systems and the Decidability Problem for Hybrid Logics
Contenu du livre :
Ce livre se situe à l'intersection de deux sujets : la décidabilité et la complexité calculatoire des logiques hybrides, et les systèmes déductifs conçus pour elles. Les logiques hybrides sont ici divisées en deux groupes : les logiques hybrides standard impliquant des nominaux en tant qu'expressions d'une sorte distincte, et les logiques hybrides non-standard, qui n'impliquent pas de nominaux mais dont le pouvoir expressif est équivalent à celui des logiques hybrides standard sans liant. Les résultats originaux de ce livre sont divisés en deux parties. Cette division reflète la division du livre lui-même. Le premier type de résultats concerne les propriétés de complexité et de théorie des modèles des logiques hybrides. Comme les logiques hybrides que nous appelons standard sont assez bien étudiées, les efforts se sont concentrés sur les logiques hybrides appelées non-standard dans ce livre. Les logiques hybrides non-standard sont comprises comme des logiques modales avec des opérateurs de comptage globaux (M(En)) dont le pouvoir expressif correspond à celui des logiques hybrides standard sans liant. Les résultats pertinents comprennent : 1. l'établissement d'une axiomatisation solide et complète pour la logique modale K avec des opérateurs de comptage globaux (MK(En)), qui peut être facilement étendue à d'autres classes de cadres, 2. l'établissement d'une axiomatisation solide et complète pour la logique modale K avec des opérateurs de comptage globaux (MK(En)).
Établissement de limites de complexité étroites, à savoir la complétude NExpTime pour la logique modale avec des opérateurs de comptage globaux définis sur les classes de cadres arbitraires, réflexifs, symétriques, sériels et transitifs (MK(En)), MT(En)), MD(En)), MB(En)), MK4(En)) avec des souscripts numériques codés en binaire. Établir la propriété de modèle de taille exponentielle pour cette logique définie sur les classes de cadres euclidiens et équivalents (MK5(En)), MS5(En)). Les résultats du second type consistent à concevoir des systèmes déductifs concrets (tableaux et séquences) pour des logiques hybrides standard et non-standard. Plus précisément, ils comprennent : 1. Concevoir un calcul de tableau préfixé et un calcul de tableau internalisé qui sont sains, complets et terminaux pour une classe riche de logiques hybrides standard sans liant. Une caractéristique intéressante des calculs indiqués est le caractère non ramifié de la règle (D), 2. la conception d'un calcul de tableau préfixé et d'un calcul de tableau internalisé qui sont sains, complets et terminaux pour les logiques hybrides non standard. La technique d'internalisation appliquée à un calcul de tableau pour la logique modale avec des opérateurs de comptage global est nouvelle dans la littérature, 3. concevoir le premier algorithme hybride impliquant un résolveur d'inégalité pour les logiques modales avec des opérateurs de comptage global. Le transfert de la partie arithmétique du raisonnement à un résolveur d'inégalités s'est avéré suffisant pour garantir la terminaison.
Le livre s'adresse aux philosophes et aux logiciens qui travaillent avec les logiques modales et hybrides, ainsi qu'aux informaticiens qui s'intéressent aux systèmes déductifs et aux procédures de décision pour les logiques. De larges fragments de la première partie du livre peuvent également servir d'introduction aux logiques hybrides pour un public plus large intéressé par la logique. Le contenu du livre se situe dans les domaines de la logique formelle et de l'informatique théorique, avec quelques éléments de la théorie de la complexité computationnelle.
Autres informations sur le livre :
| ISBN : | 9788323336952 |
| Auteur : | |
| Éditeur : | |
| Reliure : | Broché |
| Année de publication : | 2015 |
| Nombre de pages : | 232 |
Achat:
Actuellement disponible, en stock.
