The TPTP Format for Interpretations

Resumo Técnico: O Formato TPTP para Interpretações

Declaração do Problema
A Prova Automática de Teoremas (ATP) tem se concentrado historicamente na derivação de teoremas a partir de axiomas. No entanto, refutar conjecturas através da busca de contramodelos (interpretações que satisfazem os axiomas, mas falsificam a conjectura) é um aspecto crítico da ATP, essencial para aplicações como verificação formal, verificação de consistência e pesquisa operacional. Embora o mundo TPTP suporte há muito tempo um formato para interpretações tarskianas finitas, o formato existente era insuficiente para:

1. Representar interpretações com domínios infinitos.
2. Representar interpretações de Kripke (usadas em lógicas não clássicas, como a lógica modal).
3. Fornecer uma representação unificada e padronizada para interpretações de Herbrand e saturações.

A falta de um formato padronizado para esses diversos tipos de interpretação dificulta a verificação de modelos, a análise de contraexemplos e a integração da busca de modelos em fluxos de raciocínio mais amplos.

Metodologia
Os autores desenvolveram um novo formato TPTP para interpretações baseado no princípio de que as interpretações devem ser representadas como fórmulas escritas na própria linguagem TPTP. Esta abordagem aproveita a sintaxe TPTP existente (suportando CNF, FOF, TFF, THF, etc.) e a estrutura de fórmula anotada language(name, role, formula, source, useful_info).

A metodologia envolve:

• Definição do papel interpretation: Um novo papel de fórmula é introduzido para distinguir as fórmulas de interpretação dos axiomas ou conjecturas do problema.
• Estruturação de Interpretações Tarskianas: O formato define interpretações como conjunções de especificações de domínio e mapeamentos de símbolos.
  • Domínios Finitos: Especificados via disjunções universalmente quantificadas de igualdades (enumerando elementos) e restrições de distinção (usando $distinct ou termos entre aspas duplas).
  • Domínios Infinitos: Especificados via quantificação existencial para capturar disjunções infinitas (ex: números de Peano) ou através do uso de tipos definidos (ex: $int).
  • Tratamento de Tipos: Para lógicas tipadas (TFF, THF), o formato emprega "bijecções de promoção de tipo" para mapear elementos de domínio (que podem ter tipos internos distintos) para os tipos do problema, garantindo a tipagem correta.
  • Interpretações de Herbrand: Representadas usando subpapéis interpretation-herbrand, frequentemente utilizando definições de predicados sobre álgebras de termos ou saturações.
• Estruturação de Interpretações de Kripke: O formato estende a interpretação tarskiana adicionando uma camada de "mundos". Introduz símbolos definidos: $world (tipo), $accessible_world` (relação), `$local_world (constante) e $in_world (predicado). Uma interpretação de Kripke é uma conjunção que especifica o conjunto de mundos, a relação de acessibilidade e a interpretação tarskiana dentro de cada mundo.
• Granularidade e Modularidade: O formato suporta a divisão de interpretações em múltiplas fórmulas usando subpapéis (ex: interpretation-domains, interpretation-mappings) em níveis médio e fino para separar preocupações ou para representações compactas via quantificação.
• Verificação: O artigo descreve uma metodologia de verificação onde as fórmulas de interpretação são tratadas como axiomas, e as fórmulas do problema são tratadas como conjecturas (ou conjecturas negadas). Se as fórmulas do problema puderem ser provadas a partir das fórmulas de interpretação, a interpretação é verificada como um modelo válido.

Principais Contribuições

1. Sintaxe Unificada: Um formato TPTP único e extensível capaz de representar interpretações tarskianas (finitas e infinitas), de Herbrand e de Kripke.
2. Suporte a Domínios Infinitos: Mecanismos para representar domínios infinitos usando álgebras de termos (ex: números de Peano) ou tipos integrados (ex: inteiros), indo além da limitação anterior a modelos finitos.
3. Representação de Modelos de Kripke: Uma especificação formal para representar contramodelos de lógica modal, incluindo estruturas de mundos e relações de acessibilidade, dentro do framework TPTP.
4. Framework de Verificação: Um método concreto para verificar modelos reduzindo a tarefa à prova de teoremas, garantindo que a saída de um buscador de modelos não seja apenas confiável, mas verificável.
5. Ferramental e Visualização: Identificação de ferramentas que suportam o formato, incluindo o verificador de modelos AGMV e o Visualizador de Interpretação Interativo (IIV), que permite a visualização de modelos tarskianos finitos e de Kripke.

Resultos e Capacidades
O artigo não apresenta novos dados experimentais ou benchmarks, mas sim define a especificação e demonstra sua utilidade através de numerosos exemplos (fornecidos nos apêndices). Estes exemplos ilustram:

• A representação de contramodelos finitos para problemas não tipados (FOF) e tipados (TFF, THF).
• A representação de modelos infinitos usando tanto domínios de termos quanto tipos definidos.
• A representação de modelos de Kripke para lógicas não clássicas (NXF).
• A capacidade de dividir e compactar estas representações para legibilidade e modularidade.
• A construção bem-sucedida de problemas de verificação que podem ser resolvidos por sistemas de prova de teoremas confiáveis.

Significância e Alegações
Os autores afirmam que este trabalho garante que o formato de representação TPTP é adequado para as diversas necessidades da comunidade de ATP. A significância reside na mudança da busca de modelos como uma "caixa preta" para uma representação de modelo transparente, verificável e analisável.

O artigo alega modestamente que o formato fornece as propriedades necessárias para a representação de interpretações:

• Avaliabilidade: As fórmulas podem ser avaliadas em relação à interpretação.
• Tratabilidade: A avaliação é tratável para interpretações finitas; interpretações infinitas podem ser intratáveis, mas são representáveis.
• Verificabilidade: Modelos podem ser verificados checando se as fórmulas do problema seguem das fórmulas de interpretação.
• Compreensibilidade: O formato foi projetado para ser legível por humanos, embora os autores notem que representações complexas (como saturações ou domínios infinitos) podem permanecer difíceis de compreender para humanos.

O trabalho serve como uma base para que sistemas de ATP produzam modelos mais ricos e diversos, facilitando uma melhor depuração em verificação e uma análise mais profunda em pesquisa lógica. Os autores observam que o formato está sendo adotado atualmente, com planos para estendê-lo para cobrir mais linguagens não clássicas no futuro.