Trouver un modèle fini

11

Je sais que la question "est-ce qu'une formule de premier ordre a un modèle" est indécidable en général.ϕ

Quelqu'un pourrait-il me donner un lien ou un livre qui donnerait la réponse pour les modèles finis. Si j'ai une formule de premier ordre , est-il possible de déterminer si ϕ a un modèle fini? Je suis à peu près sûr que la question est bien connue, mais je ne sais même pas par où commencer la recherche d'une réponse. (Par exemple, je me serais attendu à ce que ce soit dans les "éléments de la théorie des modèles finis" de Libkin, mais il semble que je ne le trouve pas.)ϕϕ

La deuxième partie de ma question est la suivante: existe-t-il des restrictions connues pour que le problème soit décidable?

Par exemple, le problème peut devenir décidable pour une formule de premier ordre avec uniquement des prédicats monadiques. Ou quand nous avons un prédicat monadique plus une relation de successeur. Mais je ne peux pas imaginer un algorithme pour décider s'il existe un modèle (fini) sur ces restrictions.

Arthur MILCHIOR
la source
Avez-vous lu des livres sur la théorie des modèles finis?
Dave Clarke
@Dave Clarke: Livre de Libkin "Element of finite model theory" et Immerman "Descriptive
complex
Cherchez-vous le théorème de Trakhtenbrot? Pour la deuxième partie, un exemple simple est que MSO sur des mots, dénotant des langues régulières, peut être vérifié pour la satisfiabilité, car la structure des mots est elle-même quelque chose que l'on peut décrire dans MSO.
Michaël Cadilhac
Merci Michaël. Il semble bien que cela réponde à la première partie de ma question. Mais je cherche toujours ce que l'on sait des restrictions.
Arthur MILCHIOR
1
@ Michaël Cadilhac - Pourquoi ne pas poster une réponse? Le théorème de Trakhtenbrot est couvert dans le livre de Libkin au chapitre 9.
Marc Hamann

Réponses:

14

Le théorème de Trakhtenbrot répond à la première partie de votre question . La deuxième partie est en effet une question assez vaste. Selon la structure relationnelle sur laquelle vous travaillez, plusieurs solutions peuvent être proposées. Par exemple, si vous êtes intéressé par les langages formels, MSO sur les structures de mots correspond aux langages normaux, et la logique de correspondance ( voir ceci ) correspond à CFL, et donc leur problème de satisfiabilité est décidable.

Vous devriez jeter un coup d'œil au chapitre 14 de Libkin, où il est prouvé que de jolis segments de FO présentent un problème de satisfiabilité décidable, en fonction de la quantité d'alternances de quantificateurs autorisées.

Michaël Cadilhac
la source
2
Comme le dit Michaël, une grande partie de la logique de calcul semble consacrée à la recherche et à l'étude de fragments où les problèmes associés sont décidables (ou traitables). Pour ne citer qu'une belle enquête: Gottlob, Kolaitis, Schwentick, Existential second-order logic over graphs: Charting the tractability frontier , JACM 2004, dx.doi.org/10.1145/972639.972646
András Salamon
Merci pour votre réponse. Pour la question à laquelle je pensais, elle est connue pour être égale à MSO mais sur des mots imbriqués. Par conséquent, si la preuve de la décidabilité de MSO sur les mots utilise la preuve de décidabilité de l'emtpyness de CFL, cela ne m'aide pas vraiment. Et merci pour la "logique d'appariement", je ne le savais pas, mais cela ressemble beaucoup à des mots imbriqués, donc cela peut m'intéresser.
Arthur MILCHIOR
4

Je ne connais pas la réponse pour les fragments arbitraires de FO. La logique modale classique et ses extensions ont plusieurs propriétés de décidabilité. Par les traductions standard, vous obtenez des fragments de logique classique qui partagent ces propriétés.

  1. Modal Logic et le fragment invariant de bisimulation de FOL à deux variables.
  2. CTL * et le fragment invariant de bisimulation de la logique de chemin monadique.
  3. Le mu-calcul et le fragment invariant de bisimulation de la logique du second ordre monadique.

Toutes les logiques modales ci-dessus sont décidables et ont la propriété du modèle fini. D'autres logiques aux propriétés de décidabilité robustes sont le fragment gardé de FO, le fragment vaguement gardé et les logiques à point fixe gardé. Ces logiques ont été conçues pour transférer l'essence des propriétés bien comportées de la logique modale à un cadre logique classique. La logique à point fixe gardé est décidable mais n'a pas la propriété du modèle fini.

Vijay D
la source
1

Ce qui suit ne doit pas être considéré comme une vérité magistrale mais simplement comme des suggestions pour vos propres recherches. Les rédacteurs sont invités à apporter les corrections qu'ils jugent appropriées.

Premièrement, votre question intéresse apparemment la communauté des déductions automatiques. William McCune a un programme appelé Mace4 qui recherche des modèles finis. Vous voudrez peut-être lire la documentation qui décrit comment cela se fait.

En ce qui concerne les restrictions décidables spécifiques, vous souhaiterez peut-être examiner les éléments suivants:

  1. Cas où l' Univers Herbrand est fini. Une façon mécanique de vérifier un sous-ensemble de ces cas est de vérifier si la formule a des symboles de fonction. Si ce n'est pas le cas, l'Univers Herbrand est fini.

  2. Cas où l' élimination des quantificateurs est possible: theory.stanford.edu/~tingz/talks/qe.ps

Personne timide
la source
0

En plus des réponses déjà données: une très bonne référence sur la (non) décidabilité des fragments de logique du premier ordre est le livre Le problème classique de la décision de Börger, Grädel et Gurevich

fh
la source