Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates
Quelques fragments décidables de la logique du premier ordre et de l'arithmétique linéaire du premier ordre avec des prédicats non-interprétés
Résumé
First-order logic has a long tradition and is one of the most prominent and most important formalisms in computer science and mathematics. It is well-known that the satisfiability problem for full first-order logic is not solvable algorithmically — we say that first-order logic is undecidable. This fact highlights a fundamental limitation of computing devices in general and of automated reasoning in particular. The classical decision problem, as it is understood today, is the quest for a delineation between the decidable and the undecidable parts of first-order logic based on elegant and computable syntactic criteria. Many researchers have contributed to this endeavor and till today numerous decidable and undecidable fragments of first-order logic have been identified. The present thesis sheds more light on the decidability boundary and aims to open new perspectives on the already known results.
In the first part of the present thesis we focus on the syntactic concept of separateness of variables and explore its applicability to the classical decision problem and beyond. Two disjoint sets of first-order variables are separated in a given formula if each atom in that formula contains variables from at most one of the two sets. This simple notion facilitates the definition of decidable extensions of many well-known decidable first-order fragments. We shall demonstrate that for several prefix fragments, several guarded fragments, the two-variable fragment, and for the fluted fragment. Altogether, we will investigate nine such extensions more closely. Interestingly, each of them contains the monadic first-order fragment without equality. Although the extensions exhibit the same expressive power as the respective originals, certain logical properties can be expressed much more succinctly. In at least two cases the succinctness gap cannot be bounded using any elementary function. This observation can be conceived as an indication for computationally hard satisfiability problems associated with the extended fragments. Indeed, we will derive non-elementary lower bounds for an extension of the Bernays–Schönfinkel–Ramsey fragment, called the separated fragment. Furthermore, we shall investigate the effect of separateness of variables at the semantic level, where it may lead to dependences between quantified variables that are weaker than such dependences are in general. Such weak dependences will be studied in the framework of model-checking games.
The focus of the second part of the present thesis is on linear arithmetic over the rationals with uninterpreted predicates. Two novel decidable fragments shall be presented, both based on the Bernays–Schönfinkel–Ramsey fragment. On the negative side, we will identify several small fragments of the language for which satisfiability is undecidable.
La logique du premier ordre est un des formalismes les plus importants à la base des mathématiques et de l'informatique. Il est bien connu que le problème de la satisfaisabilité de la logique du premier ordre n'admet pas de solution algorithmique, et cela représente une limitation fondamentale pour les mécanismes de calcul en général et la déduction automatique en particulier. De nombreux fragments décidables ou indécidables de la logique du premier ordre ont été identifiés, et la présente thèse contribue à l'exploration de la frontière de décidabilité et donne quelques perspectives nouvelles à des résultats connus.
La première partie de la thèse se focalise sur la notion syntaxique de la séparation de variables et explore son application au problème classique de décision et au-delà. Deux ensembles disjoints de variables sont séparés dans une formule donnée si chaque sous-formule atomique ne contient de variables que dans un des deux ensembles. Cette notion simple simplifie la définition d'extensions décidables de plusieurs fragments décidables de la logique du premier ordre, ainsi que nous le montrons pour différents fragments de préfixes, des fragments gardés, le fragment à deux variables et le fragment flûté. Nous étudions neuf extensions en plus de détail et nous montrons que chacune d'elle contient la logique monadique du premier ordre sans égalité. Même si ces extensions n'augmentent pas le pouvoir expressif par rapport aux fragments d'origine, certaines propriétés logiques peuvent être exprimées de manière plus succincte, et dans deux cas au moins le degré de concision ne peut être borné par une fonction élémentaire. En effet, nous allons montrer des bornes inférieures non-élémentaires pour une extension du fragment de Bernays, Schönfinkel et Ramsey appelée le fragment séparé. Aussi nous étudions l'effet de la séparation de variables au niveau sémantique où il induit des dépendances plus faibles entre des variables quantifiées par rapport au cas général. De telles dépendances faibles seront étudiées au travers de jeux de model checking.
La seconde partie de la thèse étudie l'arithmétique linéaire de nombres rationnels en présence de prédicats non-interprétés. Deux nouveaux fragments décidables seront identifiés, comme des extensions du fragment de Bernays, Schönfinkel et Ramsey. Nous allons aussi exhiber quelques fragments du langage pour lesquels le problème de la satisfaisabilité est indécidable.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...