💻 computer science

The TPTP Format for Interpretations

Cet article introduit et détaille le format TPTP pour la représentation des interprétations tarskiennes, de Herbrand et de Kripke, en couvrant sa syntaxe, sa sémantique, sa vérification et le support d'outils afin de garantir l'adéquation pour diverses applications.

Auteurs originaux : Geoff Sutcliffe, Alexander Steen, Pascal Fontaine, Lydia Kondylidou

Publié 2026-06-02

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Geoff Sutcliffe, Alexander Steen, Pascal Fontaine, Lydia Kondylidou

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

La vue d'ensemble : Trouver le scénario du « Et si ? »

Imaginez que vous êtes un détective essayant de résoudre un mystère. Vous avez un ensemble de règles (axiomes) et une théorie (une conjecture) sur ce qui s'est passé. Habituellement, votre travail consiste à prouver que la théorie doît être vraie en se basant sur les règles.

Mais parfois, vous voulez prouver que la théorie est fausse. Pour ce faire, vous devez trouver un scénario spécifique — un « contre-exemple » — où les règles sont respectées, mais où votre théorie s'effondre. Dans le monde de la logique informatique, ce scénario est appelé une interprétation ou un modèle.

Pendant longtemps, les ordinateurs pouvaient trouver ces scénarios « faux », mais ils gardaient les résultats pour eux. Ils disaient simplement : « J'ai trouvé un contre-exemple ! » sans vous montrer à quoi il ressemblait. C'était comme un détective disant : « Le majordome ne l'a pas fait », mais refusant de vous montrer l'alibi.

Ce document présente une nouvelle façon standardisée pour les ordinateurs d'écrire ces scénarios afin que les humains et d'autres ordinateurs puissent les lire, les vérifier et les comprendre. C'est comme créer un « plan » universel pour ces réalités alternatives.

Les trois types de plans

Le document explique qu'il existe trois manières principales de construire ces scénarios, et que le nouveau format gère les trois :

1. Le monde fini (Interprétations tarskiennes)
Imaginez une petite pièce fermée avec un nombre précis de personnes et d'objets.

L'analogie : Pensez à un jeu de société comme Cluedo. Vous avez un ensemble fixe de personnages (Colonel Moutarde, Mme Peacock), un ensemble fixe de pièces et un ensemble fixe d'armes.
Le format : L'ordinateur écrit une liste : « Dans ce monde, il y a exactement 4 personnes. Le Colonel Moutarde est dans la bibliothèque. Le chandelier est dans la cuisine. » Il liste explicitement chaque connexion.
Pourquoi c'est important : C'est idéal pour vérifier si un système fonctionne avec un nombre restreint et gérable d'éléments.

2. Le monde infini (Interprétations infinies)
Maintenant, imaginez un monde qui ne finit jamais, comme la droite numérique (1, 2, 3, 4... pour toujours).

L'analogie : Vous ne pouvez pas écrire une liste infinie de nombres. À la place, vous écrivez une recette ou une règle : « Commencez par zéro. Pour obtenir le suivant, ajoutez un. »
Le format : L'ordinateur ne liste pas chaque nombre. À la place, il écrit une règle telle que : « Pour tout nombre $X$ , la personne suivante est $X+1$ . » Il utilise des formules mathématiques pour décrire la foule infinie.
Pourquoi c'est important : C'est nécessaire lorsqu'on traite des éléments comme le temps, l'argent ou des données qui peuvent croître sans limite.

3. Le multivers (Interprétations de Kripke)
Parfois, les règles changent selon l'endroit où l'on se trouve ou le moment où l'on regarde.

L'analogie : Pensez à un livre dont « vous êtes le héros » ou à un film de multivers. Dans une pièce (Monde A), il pleut. Dans la pièce suivante (Monde B), il fait beau. Les personnages peuvent être différents dans chaque pièce, ou rester les mêmes. Il y a des portes reliant ces pièces (accessibilité).
Le format : L'ordinateur dessine une carte de toutes les pièces, quelles portes sont ouvertes et quel temps il fait dans chaque pièce. Il dit : « Dans le Monde 1, il pleut. Dans le Monde 2, il fait beau. Vous pouvez passer du Monde 1 au Monde 2, mais pas l'inverse. »
Pourquoi c'est important : C'est crucial pour des choses comme les protocoles de sécurité ou le raisonnement de l'IA, où la vérité dépend du contexte.

La « Recette » du format

Le document détaille précisément comment écrire ces plans en utilisant un langage spécifique appelé TPTP. Considérez le TPTP comme un langage de programmation universel pour la logique.

Les ingrédients : Le format nécessite de définir le « domaine » (qui est dans la pièce), les « correspondances » (qui fait quoi) et les « règles » (ce qui est vrai ou faux).
La flexibilité : Le format est intelligent. Il peut être à grain grossier (un grand paragraphe désordonné décrivant tout le monde) ou à grain fin (un tableau détaillé détaillant chaque personne et chaque objet).
Le cas particulier « Herbrand » : Parfois, le « monde » n'est qu'une liste de mots et de phrases générée par l'ordinateur lui-même. Le document appelle cela des « interprétations de Herbrand ». C'est comme un dictionnaire dont les définitions sont entièrement construites à partir des mots du dictionnaire.

Pourquoi en avons-nous besoin ? (Le problème du « Faites-moi confiance »)

Le document soutient que trouver une solution ne suffit pas ; nous devons la vérifier.

L'ancienne méthode : Un ordinateur dit : « J'ai trouvé un bug ! ». Vous devez faire confiance à l'ordinateur. Si l'ordinateur a fait une erreur, vous êtes coincé avec un système défectueux.
La nouvelle méthode : L'ordinateur vous remet le plan (l'interprétation). Vous (ou un autre ordinateur) pouvez lire le plan et vérifier les calculs.
- Pouvez-vous le lire ? Oui, le format est conçu pour être lisible par l'humain.
- Pouvez-vous le vérifier ? Oui, vous pouvez exécuter un test simple pour voir si le plan respecte réellement les règles.
- Est-ce utile ? Oui, car si vous trouvez un bug, le plan montre exactement où se situe la faute (ex: « John est dans la cuisine, mais les règles disent qu'il devrait être dans la bibliothèque »).

La « Boîte à outils »

Le document mentionne que des outils existent déjà pour aider :

Visualiseurs : Imaginez une carte en 3D où vous pouvez cliquer sur un « Monde » et voir les personnages à l'intérieur. Le document mentionne un outil appelé « Interactive Interpretation Viewer » (IIV) qui fait exactement cela pour les mondes finis.
Vérificateurs : Des outils qui prennent le plan et les règles originales et vérifient automatiquement s'ils correspondent.

Résumé

En bref, ce document traite de la standardisation de la manière dont les ordinateurs partagent leurs scénarios de « et si ? ».

Avant, les ordinateurs trouvaient des contre-exemples mais les gardaient cachés dans une boîte noire. Désormais, ils peuvent les écrire sous la forme d'un « plan » clair et standardisé. Cela permet aux humains de regarder le plan, de comprendre pourquoi un système a échoué et de vérifier que l'ordinateur n'a pas fait d'erreur. Cela transforme un moment de « faites-moi confiance » en un moment de « montrez-le moi ».

Résumé technique : Le format TPTP pour les interprétations

Énoncé du problème
La preuve automatique de théorèmes (ATP - Automated Theorem Proving) s'est historiquement concentrée sur la déduction de théorèmes à partir d'axiomes. Cependant, l'infirmation de conjectures par la recherche de contre-modèles (des interprétations qui satisfont les axiomes mais falsifient la conjecture) est un aspect crucial de l'ATP, essentiel pour des applications telles que la vérification formelle, la vérification de cohérence et la recherche opérationnelle. Bien que le monde TPTP supporte depuis longtemps un format pour les interprétations tarskiennes finies, le format existant était insuffisant pour :

Représenter des interprétations avec des domaines infinis.
Représenter des interprétations de Kripke (utilisées dans les logiques non classiques comme la logique modale).
Fournir une représentation unifiée et standardisée des interprétations de Herbrand et des saturations.

L'absence d'un format standardisé pour ces divers types d'interprétations entrave la capacité de vérifier les modèles, d'analyser les contre-exemples et d'intégrer la recherche de modèles dans des pipelines de raisonnement plus larges.

Méthodologie
Les auteurs ont développé un nouveau format TPTP pour les interprétations basé sur le principe selon lequel les interprétations doivent être représentées sous forme de formules écrites dans le langage TPTP lui-même. Cette approche tire parti de la syntaxe TPTP existante (supportant CNF, FOF, TFF, THF, etc.) et de la structure de formule annotée langage(nom, rôle, formule, source, info_utile).

La méthodologie implique :

Définition du rôle interpretation : Un nouveau rôle de formule est introduit pour distinguer les formules d'interprétation des axiomes ou des conjectures du problème.
Structuration des interprétations tarskiennes : Le format définit les interprétations comme des conjonctions de spécifications de domaines et de mappages de symboles.
- Domaines finis : Spécifiés via des disjonctions universellement quantifiées d'égalités (énumération des éléments) et de contraintes de distinction (utilisant $distinct ou des termes entre guillemets doubles).
- Domaines infinis : Spécifiés via la quantification existentielle pour capturer des disjonctions infinies (par exemple, les nombres de Peano) ou en utilisant des types définis (par exemple, $int).
- Gestion des types : Pour les logiques typées (TFF, THF), le format emploie des « bijections de promotion de type » pour mapper les éléments du domaine (qui peuvent avoir des types internes distincts) vers les types du problème, assurant ainsi la conformité de type.
- Interprétations de Herbrand : Représentées à l'aide de sous-rôles interpretation-herbrand, utilisant souvent des définitions de prédicats sur des algèbres de termes ou des saturations.
Structuration des interprétations de Kripke : Le format étend l'interprétation tarskienne en ajoutant une couche de « mondes ». Il introduit des symboles définis : $world (type), $accessible_world` (relation), `$ local_world (constante), et $in_world (prédicat). Une interprétation de Kripke est une conjonction spécifiant l'ensemble des mondes, la relation d'accessibilité, et l'interprétation tarskienne au sein de chaque monde.
Granularité et modularité : Le format permet de diviser les interprétations en plusieurs formules en utilisant des sous-rôles (par exemple, interpretation-domains, interpretation-mappings) à des niveaux de granularité moyenne et fine pour séparer les préoccupations ou pour des représentations compactes via la quantification.
Vérification : Le document expose une méthodologie de vérification où les formules d'interprétation sont traitées comme des axiomes, et les formules du problème sont traitées comme des conjectures (ou des négations de conjectures). Si les formules du problème peuvent être prouvées à partir des formules d'interprétation, l'interprétation est vérifiée comme un modèle valide.

Contributions clés

Syntaxe unifiée : Un format TPTP unique et extensible capable de représenter des interprétations de Tarski (finies et infinies), de Herbrand et de Kripke.
Support des domaines infinis : Mécanismes pour représenter des domaines infinis en utilisant des algèbres de termes (ex: nombres de Peano) ou des types intégrés (ex: entiers), dépassant la limitation précédente aux modèles finis.
Représentation de modèles de Kripke : Une spécification formelle pour représenter les contre-modèles de la logique modale, incluant les structures de mondes et les relations d'accessibilité, au sein du cadre TPTP.
Cadre de vérification : Une méthode concrète pour vérifier les modèles en réduisant la tâche à la preuve de théorèmes, garantissant que la sortie d'un chercheur de modèles n'est pas seulement digne de confiance, mais vérifiable.
Outillage et visualisation : Identification d'outils supportant le format, notamment le vérificateur de modèles AGMV et l'Interactive Interpretation Viewer (IIV), qui permet la visualisation de modèles tarskiens finis et de Kripke.

Résultats et capacités
Le document ne présente pas de nouvelles données expérimentales ou de benchmarks, mais définit plutôt la spécification et démontre son utilité à travers de nombreux exemples (fournis dans les appendices). Ces exemples illustrent :

La représentation de contre-modèles finis pour des problèmes non typés (FOF) et typés (TFF, THF).
La représentation de modèles infinis utilisant à la fois des domaines de termes et des types définis.
La représentation de modèles de Kripke pour les logiques non classiques (NXF).
La capacité de diviser et de compacter ces représentations pour la lisibilité et la modularité.
La construction réussie de problèmes de vérification qui peuvent être épuisés par des systèmes ATP de confiance.

Signification et affirmations
Les auteurs affirment que ce travail garantit que le format de représentation TPTP est adéquat pour les besoins diversifiés de la communauté ATP. La signification réside dans le passage d'une recherche de modèle en « boîte noire » à une représentation de modèle transparente, vérifiable et analysable.

Le document affirme modestement que le format fournit les propriétés nécessaires pour la représentation d'interprétations :

Évaluabilité : Les formules peuvent être évaluées par rapport à l'interprétation.
Tractabilité : L'évaluation est tractable pour les interprétations finies ; les interprétations infinies peuvent être intraitables mais sont représentables.
Vérifiabilité : Les modèles peuvent être vérifiés en vérifiant si les formules du problème découlent des formules d'interprétation.
Compréhensibilité : Le format est conçu pour être lisible par l'humain, bien que les auteurs notent que les représentations complexes (comme les saturations ou les domaines infinis) puissent rester difficiles à comprendre pour l'homme.

Ce travail sert de fondation pour que les systèmes ATP produisent des modèles plus riches et plus diversifiés, facilitant un meilleur débogage dans la vérification et une analyse plus profonde dans la recherche en logique. Les auteurs notent que le format est actuellement en cours d'adoption, avec des plans pour l'étendre afin de couvrir davantage de langages non classiques à l'avenir.