💻 computer science

The TPTP Format for Interpretations

Dit artikel introduceert en beschrijft het TPTP-formaat voor het representeren van Tarskische, Herbrand- en Kripke-interpretaties, waarbij de syntaxis, semantiek, verificatie en tool-ondersteuning worden behandeld om de geschiktheid voor diverse toepassingen te waarborgen.

Oorspronkelijke auteurs: Geoff Sutcliffe, Alexander Steen, Pascal Fontaine, Lydia Kondylidou

Gepubliceerd 2026-06-02

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Geoff Sutcliffe, Alexander Steen, Pascal Fontaine, Lydia Kondylidou

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Het Grote Plaatje: Het "Wat als"-scenario vinden

Stel je voor dat je een detective bent die een mysterie probeert op te lossen. Je hebt een reeks regels (axioma's) en een theorie (een conjectuur) over wat er is gebeurd. Normaal gesproken is je taak om te bewijzen dat de theorie waar moet zijn op basis van de regels.

Maar soms wil je juist bewijzen dat de theorie onjuist is. Om dat te doen, moet je een specifiek scenario vinden — een "tegenvoorbeeld" — waarin de regels wel waar zijn, maar je theorie niet klopt. In de wereld van de computercode wordt dit scenario een interpretatie of een model genoemd.

Lange tijd konden computers deze "onjuiste" scenario's wel vinden, maar hielden ze de resultaten voor zichzelf. Ze zeiden alleen: "Ik heb een tegenvoorbeeld gevonden!" zonder te laten zien hoe dat eruitzag. Dit was alsof een detective zegt: "De butler heeft het niet gedaan," maar vervolgens weigert het alibi te tonen.

Dit artikel introduceert een nieuwe, gestandaardiseerde manier voor computers om deze scenario's op te schrijven, zodat mensen en andere computers ze kunnen lezen, controleren en begrijpen. Het is also af een universele "blauwdruk" voor deze alternatieve realiteiten.

De Drie Soorten Blauwdrukken

Het artikel legt uit dat er drie belangrijke manieren zijn om deze scenario's te bouwen, en het nieuwe formaat handelt alle drie af:

1. De Eindige Wereld (Tarskiaanse Interpretaties)
Stel je een kleine, afgesloten kamer voor met een specifief aantal mensen en objecten.

De Analogie: Denk aan een bordspel zoals Cluedo. Je hebt een vaste set personages (Kolonel Mosterd, Mevrouw Peacock), een vaste set kamers en een vaste set wapens.
Het Formaat: De computer schrijft een lijst op: "In deze wereld zijn precies 4 mensen. Kolonel Mosterd is in de bibliotheek. De kandelaar staat in de keuken." Het somt expliciet elke enkele verbinding op.
Waarom het belangrijk is: Dit is ideaal om te controleren of een systeem werkt met een klein, beheersbaar aantal items.

2. De Oneindige Wereld (Oneindige Interpretaties)
Stel je nu een wereld voor die nooit eindigt, zoals de getallenlijn (1, 2, 3, 4... voor eeuwig).

De Analogie: Je kunt geen oneindige lijst met getallen opschrijven. In plaats daarvan schrijf je een recept of een regel: "Begin bij nul. Om het volgende getal te krijgen, tel je er één bij op."
Het Formaat: De computer schrijft niet elk getal op. In plaats daarvan gebruikt de computer een regel zoals: "Voor elk getal $X$ is de volgende persoon $X+1$ ." Het gebruikt wiskundige formules om de oneindige menigte te beschrijven.
Waarom het belangrijk is: Dit is nodig bij zaken als tijd, geld of data die zonder limiet kunnen groeien.

3. Het Multiversum (Kripke Interpretaties)
Soms veranderen de regels afhankelijk van waar je bent of wanneer je kijkt.

De Analogie: Denk aan een "Kies je eigen avontuur"-boek of een multiversum-film. In één kamer (Wereld A) regent het. In de volgende kamer (Wereld B) is het zonnig. De personages kunnen verschillen in elke kamer, of ze kunnen hetzelfde blijven. Er zijn deuren die deze kamers verbinden (toegankelijkheid).
Het Formaat: De computer schrijft een kaart van alle kamers, welke deuren openstaan en wat het weer is in elke kamer. Het zegt: "In Wereld 1 regent het. In Wereld 2 is het zonnig. Je kunt van Wereld 1 naar Wereld 2 lopen, maar niet terug."
Waarom het belangrijk is: Dit is cruciaal voor zaken als beveiligingsprotocollen of AI-redeneringen, waarbij de waarheid afhangt van de context.

Het "Recept" voor het Formaat

Het artikel beschrijft precies hoe je deze blauwdrukken schrijft met behulp van een specifieke taal genaamd TPTP. Zie TPTP als een universele programmeertaal voor logica.

De Ingrediënten: Het formaat vereist dat je de "domein" definieert (wie is er in de kamer), de "mappings" (wie doet wat) en de "regels" (wat is waar of onwaar).
De Flexibiliteit: Het formaat is slim. Het kan grofmazig zijn (een grote, rommelige paragraaf die de hele wereld beschrijft) of fijnmazig (een gedetailleerd spreadsheet dat elke persoon en elk object uitsplitst).
Het "Herbrand" Speciale Geval: Soms is de "wereld" gewoon een lijst met woorden en zinnen die de computer zelf genereert. Het artikel noemt deze "Herbrand-interpretaties". Het is als een woordenboek waarbij de definities volledig zijn opgebouwd uit de woorden in het woordenboek zelf.

Waarom hebben we dit nodig? (Het "Vertrouw mij"-probleem)

Het artikel stelt dat het vinden van een oplossing alleen niet genoeg is; we moeten het ook verifiëren.

De Oude Manier: Een computer zegt: "Ik heb een bug gevonden!" Je moet de computer vertrouwen. Als de computer een fout maakt, zit je vast met een defect systeem.
De Nieuwe Manier: De computer overhandigt je de blauwdruk (de interpretatie). Jij (of een andere computer) kunt de blauwdruk lezen en de wiskunde controleren.
- Kun je het lezen? Ja, het formaat is ontworpen om menselijk leesbaar te zijn.
- Kun je het controleren? Ja, je kunt een eenvoudige test draaien om te zien of de blauwdruk de regels daadwerkelijk laat kloppen.
- Is het nuttig? Ja, want als je een bug vindt, laat de blauwdruk je precies zien waar de fout zit (bijv. "John is in de keuken, maar de regels zeggen dat hij in de bibliotheek zou moeten zijn").

De "Toolbox"

Het artikel vermeldt dat er al hulpmiddelen bestaan om hiermee te helpen:

Visualisaties: Stel je een 3D-kaart voor waar je op een "Wereld" kunt klikken en de personages daarin kunt zien. Het artikel noemt een tool genaamd de "Interactive Interpretation Viewer" (IIV) die dit precies doet voor eindige werelden.
Verifiers (Verifieerders): Tools die de blauwdruk en de oorspronkelijke regels nemen en automatisch controleren of deze overeenkomen.

Samenvatting

Kortom, dit artikel gaat over het standaardiseren van de manier waarop computers hun "wat als"-scenario's delen.

Voorheen vonden computers tegenvoorbeelden, maar hielden ze deze verborgen in een zwarte doos. Nu kunnen ze ze opschrijven in een duidelijke, gestandaardiseerde "blauwdruk"-taal. Dit stelt mensen in staat om naar de blauwdruk te kijken, te begrijpen waarom een systeem faalde en te verifiëren of de computer geen fout heeft gemaakt. Het verandert een "vertrouw mij"-moment in een "laat het me zien"-moment.

Technische Samenvatting: Het TPTP-formaat voor Interpretaties

Probleemstelling
Automated Theorem Proving (ATP) heeft historisch gezien de nadruk gelegd op het afleiden van stellingen uit axioma's. Het weerleggen van vermoedens door tegenmodellen te vinden (interpretaties die axioma's bevredigen maar de vermoedens falsificeren) is echter een cruciaal aspect van ATP, essentieel voor toepassingen zoals formele verificatie, consistentiecontrole en operations research. Hoewel de TPTP-wereld al lang een formaat ondersteunt voor eindige Tarskische interpretaties, was het bestaande formaat onvoldoende voor:

Het representeren van interpretaties met oneindige domeinen.
Het representeren van Kripke-interpretaties (gebruikt in niet-klassieke logica zoals modale logica).
Het bieden van een verenigde, gestandaardiseerde representatie voor Herbrand-interpretaties en saturaties.

Het gebrek aan een gestandaardiseerd formaat voor deze diverse typen interpretaties belemmert de mogelijkheid om modellen te verifiëren, tegenvoorbeelden te analyseren en modelvinding te integreren in bredere redeneerpipelines.

Methodologie
De auteurs hebben een nieuw TPTP-formaat voor interpretaties ontwikkeld op basis van het principe dat interpretaties moeten worden gerepresenteerd als formules geschreven in de TPTP-taal zelf. Deze aanpak maakt gebruik van de bestaande TPTP-syntaxis (ondersteuning voor CNF, FOF, TFF, THF, etc.) en de geannoteerde formule-structuur language(name, role, formula, source, useful_info).

De methodologie omvat:

Het definiëren van de interpretation-rol: Een nieuwe formule-rol wordt geïntroduceerd om interpretatie-formules te onderscheiden van probleem-axioma's of vermoedens.
Het structureren van Tarskische interpretaties: Het formaat definieert interpretaties als conjuncties van domeinspecificaties en symbool-mappings.
- Eindige domeinen: Gespecificeerd via universeel gekwantificeerde disjuncties van gelijkheden (het enumereren van elementen) en distinctheid-beperkingen (met behulp van $distinct of dubbel aangequoteerde termen).
- Oneindige domeinen: Gespecificeerd via existentiële kwantificatie om oneindige disjuncties te vatten (bijv. Peano-getallen) of door gebruik te maken van gedefinieerde typen (bijv. $int).
- Type-afhandeling: Voor getypeerde logica's (TFF, THF) gebruikt het formaat "type-promotie bijeenhangendheden" (type-promotion bijections) om domeinelementen (die verschillende interne typen kunnen hebben) te mappen naar de typen van het probleem, om welgetypeerdheid te garanderen.
- Herbrand-interpretaties: Gerepresenteerd met behulp van interpretation-herbrand subrollen, vaak gebruikmakend van predicaat-definities over term-algebra's of saturaties.
Het structureren van Kripke-interpretaties: Het formaat breidt de Tarskische interpretatie uit door een laag van "werelden" toe te voegen. Het introduceert gedefinieerde symbolen: $world (type), $accessible_world` (relatie), `$ local_world (constante) en $in_world (predicaat). Een Kripke-interpretatie is een conjunctie die de verzameling werelden, de toegankelijkheidsrelatie en de Tarskische interpretatie binnen elke wereld specificeert.
Granulariteit en Modulariteit: Het formaat ondersteunt het splitsen van interpretaties in meerdere formules met behulp van subrollen (bijv. interpretation-domains, interpretation-mappings) op medium en fijnmazig niveau om zorgen te scheiden of compacte representaties te maken via kwantificatie.
Verificatie: De auteurs schetsen een verificatiemethodologie waarbij de interpretatie-formules als axioma's worden behandeld en de oorspronkelijke probleem-formules als vermoedens (of negatieve vermoedens). Als de probleem-formules bewezen kunnen worden vanuit de interpretatie-formules, dan is de interpretatie een geldige interpretatie.

Belangrijkste Bijdragen

Verenigde Syntaxis: Eén enkel, uitbreidbaar TPTP-formaat dat in staat is om Tarskische (eindige en oneindige), Herbrand en Kripke-interpretaties te representeren.
Ondersteuning voor Oneindige Domeinen: Mechanismen om oneindige domeinen te representeren met behulp van term-algebra's (bijv. Peano-getallen) of ingebouwde typen (bijv. gehele getallen), waarmee de eerdere beperking tot eindige modellen wordt overwonnen.
Kripke-model Representatie: Een formele specificatie voor het representeren van modale logica tegenmodellen, inclusclusief wereldstructuren en toegankelijkheidsrelaties, binnen het TPTP-raamwerk.
Verificatiekader: Een concrete methode voor het verifiëren van modellen door de taak te reduceren tot stellingbewijzen, waardoor wordt gewaarborgd dat de output van een modelvinder niet louter vertrouwd, maar verifieerbaar is.
Tooling en Visualisatie: Identificatie van tools die het formaat ondersteunen, waaronder de AGMV model-verifieerder en de Interactive Interpretation Viewer (IIV), die de visualisatie van eindige Tarskische en Kripke-modellen mogelijk maakt.

Resultaten en Mogelijkheden
Het artikel presenteert geen nieuwe experimentele data of benchmarks, maar definieert de specificatie en demonstreert de bruikbaarheid ervan door middel van talrijke voorbeelden (geleverd in de bijlagen). Deze voorbeelden illustreren:

De representatie van eindige tegenmodellen voor ongetypeerde (FOF) en getypeerde (TFF, THF) problemen.
De representatie van oneindige modellen met behulp van zowel term-domeinen als gedefinieerde typen.
De representatie van Kripke-modellen voor niet-klassieke logica (NXF).
Het vermogen om deze representaties te splitsen en te compacteren voor leesbaarheid en modulariteit.
De succesvolle constructie van verificatieproblemen die kunnen worden afgehandeld door vertrouwde ATP-systemen.

Betekenis en Claims
De auteurs stellen dat dit werk ervoor zorgt dat de TPTP-representatie-formaat adequaat is voor de diverse behoeften van de ATP-gemeenschap. De betekenis ligt in de verschuiving van "black box" modelvinding naar transparante, verifieerbare en analyseerbare modelrepresentatie.

Het artikel claimt bescheiden dat het formaat de noodzakelijke eigenschappen biedt voor interpretatie-representatie:

Evalueerbaarheid: Formules kunnen worden geëvalueerd met betrekking tot de interpretatie.
Tractabiliteit: Evaluatie is tractabel voor eindige interpretaties; oneindige interpretaties kunnen intratabel zijn maar zijn wel representeerbaar.
Verifieerbaarheid: Modellen kunnen worden geverifieerd door te controleren of de probleem-formules volgen uit de interpretatie-formules.
Begrijpelijkheid: Het formaat is ontworpen om menselijk leesbaar te zijn, hoewel de auteurs opmerken dat complexe representaties (zoals saturaties of oneindige domeinen) voor mensen nog steeds moeilijk te begrijpen kunnen zijn.

Dit werk dient als fundament voor ATP-systemen om rijkere, diversere modellen uit te voeren, wat beter debuggen in verificatie en diepere analyse in logisch onderzoek faciliteert. De auteurs merken op dat het formaat momenteel wordt geadopteerd, met plannen om het uit te breiden naar meer niet-klassieke talen in de toekomst.