Logique gardée - Guarded logic

La logique gardée est un ensemble de choix de logique dynamique impliquée dans des choix, où les résultats sont limités.

Un exemple simple de logique gardée est le suivant : si X est vrai, alors Y, sinon Z peut être exprimé en logique dynamique par (X?;Y)∪(~X?;Z). Cela montre un choix logique gardé : si X est vérifié, alors X?;Y est égal à Y, et ~X?;Z est bloqué, et Y∪block est également égal à Y. Par conséquent, lorsque X est vrai, l'interprète principal de l'action ne peut prendre que la branche Y, et lorsqu'elle est fausse, la branche Z.

Un exemple concret est l'idée de paradoxe : quelque chose ne peut pas être à la fois vrai et faux. Un choix logique gardé est un choix où tout changement de vrai affecte toutes les décisions prises sur toute la ligne.

Histoire

Avant l'utilisation de la logique protégée, deux termes principaux étaient utilisés pour interpréter la logique modale. La logique mathématique et la théorie des bases de données (intelligence artificielle) étaient la logique des prédicats du premier ordre. Les deux termes ont trouvé des sous-classes de logique de première classe et efficacement utilisés dans des langages résolvables qui peuvent être utilisés pour la recherche. Mais ni l'un ni l'autre ne pouvait expliquer de puissantes extensions de point fixe aux logiques de style modal.

Plus tard, Moshe Y. Vardi a émis l'hypothèse qu'un modèle d'arbre fonctionnerait pour de nombreuses logiques de style modal. Le fragment gardé de la logique du premier ordre a été introduit pour la première fois par Hajnal Andréka , István Németi et Johan van Benthem dans leur article Langages modaux et fragments bornés de logique des prédicats. Ils ont réussi à transférer les propriétés clés de la description , de la logique modale et temporelle à la logique des prédicats. Il a été constaté que la décidabilité robuste de la logique gardée pouvait être généralisée avec une propriété de modèle d'arbre. Le modèle arborescent peut également être une indication forte que la logique gardée étend le cadre modal qui conserve les bases des logiques modales.

Les logiques modales sont généralement caractérisées par des invariances sous bisimulation . Il se trouve aussi que l'invariance sous bisimulation est la racine de la propriété du modèle d'arbre qui aide à définir la théorie des automates .

Types de logique gardée

Dans Guarded Logic, il existe de nombreux objets gardés. Le premier fragment étant gardé qui est la logique du premier ordre de la logique modale. Les fragments gardés généralisent la quantification modale en trouvant des modèles relatifs de quantification. La syntaxe utilisée pour désigner le fragment gardé est GF . Un autre objet est une logique de point fixe gardé notée μGF étend naturellement le fragment gardé des points fixes du plus petit au plus grand. Les bisimulations gardées sont des objets qui, lors de l'analyse de la logique gardée. Toutes les relations dans une algèbre relationnelle standard légèrement modifiée avec bisimulation gardée et définissables au premier ordre sont appelées algèbre relationnelle gardée . Ceci est noté à l'aide de GRA .

Outre les objets logiques protégés de premier ordre, il existe des objets de logique protégée de second ordre. Elle est connue sous le nom de logique de second ordre gardée et notée GSO . Semblable à la logique du second ordre , la logique du second ordre gardée quantifie dont la plage sur les relations gardées la restreint sémantiquement. Ceci est différent de la logique du second ordre dont la plage est restreinte à des relations arbitraires.

Définitions de la logique gardée

Soit B une structure relationnelle d'univers B et de vocabulaire τ.

i) Un ensemble X ⊆ B est gardé dans B s'il existe un atome fondamental α(b_1, ..., b_k) dans B tel que X = {b_1, ..., b_k}.

ii) Une -structure A , en particulier une sous-structure A ⊆ B, est gardée si son univers est un ensemble gardé dans A (dans B ).

iii) Un tuple (b_1, ..., b_n) ∈ B^n est gardé dans B si {b_1, ..., b_n} ⊆ X pour un certain ensemble gardé X ⊆ B.

iv) Un tuple (b_1, ..., b_k) B^k est une liste gardée dans B si ses composantes sont deux à deux distinctes et {b_1, ..., b_k} est un ensemble gardé. La liste vide est considérée comme une liste gardée.

v) Une relation X B^n est gardée si elle n'est constituée que de tuples gardés.

Bisimulation gardée

Une bisimulation gardée entre deux -structures A et B est un ensemble non vide I d'isomorphes partiels finis f : X → Y de A vers B tel que les conditions de va-et-vient sont satisfaites.

Retour : Pour tout f : X → Y dans I et pour tout ensemble gardé Y` ⊆ B , il existe un isomorphe partiel g : X` → Y` dans I tel que f^-1 et g^-1 s'accordent sur Y ∩ Y' .

Quatrième Pour tout f : X → Y dans I et pour tout ensemble gardé X` ⊆ A , il existe un isomorphe partiel g : X` → Y` dans I tel que f et g s'accordent sur X ∩ X` .

Les références