Représente des termes syntaxiquement différents dans TPTP

Question

Je jette un coup d'oeil aux démonstrateurs de théorème de logique du premier ordre tels que Vampire et E-Prover, et la syntaxe de TPTP semble être la voie à suivre. Je suis plus familier avec les syntaxes de Programmation Logique telles que Answer Set Programming et Prolog, et bien que j'essaie de me référer à la description détaillée du TPTP syntax, je ne sais toujours pas comment distinguer correctement le foncteur interprété et non interprété (et je pourrais utiliser la terminologie erronée). Essentiellement, j'essaie de prouver un théorème en montrant qu'aucun modèle n'agit comme un contre-exemple. Ma première difficulté était que je ne m'attendais pas à ce que le programme logique suivant soit satisfaisant.

fof(all_foo, axiom, ![X] : (pred(X) => (X = foo))). 
fof(exists_bar, axiom, pred(bar)). 

Il est en effet satisfiable parce que rien n'empêche bar d'être égal à foo. Donc une première solution serait d'insister sur le fait que ces deux termes sont distincts et nous obtenons le programme insatisfiable suivant.

fof(all_foo, axiom, ![X] : pred(X) => (X = foo)). 
fof(exists_bar, axiom, pred(bar)). 
fof(foo_not_bar, axiom, foo != bar). 

Le rapport précise que techinal différentes chaînes entre guillemets sont des objets différents en effet, si une autre solution est de mettre des guillemets ici et là, afin d'obtenir le programme suivant insatisfiable. Je suis heureux de ne pas avoir spécifié manuellement l'inégalité car cela ne serait évidemment pas à l'échelle d'un scénario plus réaliste. En me rapprochant de ma situation réelle, je dois gérer des termes composés, et le programme suivant est malheureusement satisfaisant.

fof(all_foo, axiom, ![X] : (pred(X) => (X = f("foo")))). 
fof(exists_bar, axiom, pred(g("bar"))). 

Je suppose que f("foo") est pas un terme, mais la fonction f appliquée à l'objet "foo". Il pourrait donc coïncider avec la fonction g. Bien qu'une spécification manuelle qui f et g ne coïncide jamais, le programme suivant est insatisfiable, je me sens comme je le fais mal. Et il ne s'agirait probablement pas de mon véritable environnement avec beaucoup de termes à interpréter comme distincts quand ils sont syntaxiquement distincts. J'ai essayé de lancer des guillemets simples, mais je n'ai pas trouvé la bonne façon de le faire. Comment faire des termes (composés) syntaxiquement différents et tester l'égalité syntaxique? Question subsidiaire: le programme suivant est satisfiable, car le prouveur de théorème automatisé comprend f comme une fonction plutôt qu'un foncteur non interprété.

fof(exists_f_g, axiom, (?[I] : ((f(foo) = f(I)) & pred(g(I))))). 
fof(not_g_foo, axiom, ~pred(g(foo))). 

Pour le rendre insatisfiable, je dois spécifier manuellement que f est injective. Quel serait le moyen naturel d'obtenir ce comportement sans spécifier l'injectivité de tous les foncteurs qui se produisent dans mon programme?

fof(exists_f_g, axiom, (?[I] : ((f(foo) = f(I)) & pred(g(I))))). 
fof(not_g_foo, axiom, ~pred(g(foo))). 
fof(f_injective, axiom, ![X,Y] : (f(X) = f(Y) => (X = Y))). 

Answer 1

tout d'abord permettez-moi de vous indiquer la Syntax BNF de TPTP. En principe, vous avez des termes Prolog avec des opérateurs infixes/préfixes prédéfinis de précédences appropriées. Cela signifie que les variables sont écrites en majuscules et que les constantes sont écrites en minuscules. De même que Prolog, l'échappement avec des guillemets simples nous permet d'écrire une constante commençant par une lettre majuscule, c'est-à-dire 'X'.Je n'ai jamais vu de doubles atomes cités jusqu'ici, alors vous pourriez vouloir consulter les instructions du prouveur sur la façon de les interpréter.

Mais même si la syntaxe est Prolog-ish, la démonstration automatique du théorème est un type de bête différent. Il n'y a aucune hypothèse mondiale fermée ne sont différentes constantes supposées être différentes - c'est la raison pour laquelle vous ne trouvez pas une preuve pour:

fof(c1, conjecture, a=b). 

et ni pour:

fof(c1, conjecture, ~(a=b)). 

Donc, si vous voulez avoir dis syntaxiques -égalité, vous devez l'axiomatiser. Maintenant, supposer un différent de b montre trivialement qu'ils sont différents, j'ai donc au moins affirmé: "Supposons qu'il y ait deux constantes différentes a et b, alors il existe une variable qui n'est pas b."

fof(a1, axiom, ~(a=b)). 
fof(c1, conjecture, ?[X]: ~(X=b)). 

Depuis des fonctions dans la logique du premier ordre ne sont pas nécessairement injective, vous ne recevez pas aussi autour d'ajouter votre hypothèse là-dedans.

Veuillez également noter les différents rôles des formules d'entrée: jusqu'à présent vous avez seulement énoncé des axiomes et aucune conjecture, c'est-à-dire que vous demandez au prouveur de montrer que votre axiome est incohérent. Certains prouveurs peuvent même abandonner parce qu'ils utilisent des raffinements de résolution (par exemple un ensemble de support) qui limitent la résolution entre les axiomes [1]. Dans tous les cas, vous devez être conscient que la formule que vous essayez de prouver est de la forme A1 ∧ ... ∧ An → C1 ∨ ... Cm où les A sont des axiomes et les C sont des conjectures. [2] J'espère que la syntaxe est au moins un peu plus claire maintenant - malheureusement, la réponse aux questions est que les prouveurs de théorèmes atomisés ne font pas les mêmes suppositions que vous attendez, donc vous devez les axiomatiser. Ces axiomatizations sont souvent inefficaces et vous pourriez obtenir de meilleurs résultats avec des outils spécialisés.

[1] Comme vous l'avez déjà remarqué, les prouveurs avancés tels que Vampire ou E Prover vous renseignent sur la (contre-) satisfaction à la place. Un prouveur de théorème basé sur la résolution annulera d'abord cette formule et effectuera une transformation CNF, mais même si la plupart des prouveurs acceptant TPTP sont basés sur la résolution, ce n'est pas une exigence.