Trouver un modèle fini

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

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.)$\phi$$\phi$

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.

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.

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.

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

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