Comment la skolemisation des clauses EXISTS solitaires fonctionne-t-elle?

Question

Si j'ai une formule comme:

FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y)) 

(FA = pour tous/E = Existant)

Les règles de skolemisation dire que:

1. si E est en dehors de FA remplacer par une constante ou
2. si E est à l'intérieur de FA remplacer par une nouvelle fonction contient toutes les variables de l'extérieur du FA en tant qu'arguments.

Alors qu'est-ce que je fais dans ce cas? Puis-je simplement supprimer le quantificateur Exists ou le remplacer par une constante?

Merci!

Answer 1

d'abord écrire cela en utilisant la notation standard:

∀x∀y(∃z(!A(x,z)∨!A(y,z))∨B(x,y)) 

Maintenant, l'application de votre deuxième règle de skolemisation:

∀x∀y((!A(x,f(x,y))∨!A(y,f(x,y)))∨B(x,y)) 

J'ai remplacé ∃z avec une fonction contenant tous vars de l'extérieur. Maintenant, ce n'est pas encore sous forme normale Skolem, car il n'est pas en conjective forme normale prenex: les formules utilisent encore beaucoup de disjonctions (∨). Enlever ceux-ci est laissé à vous.