Fragment (logique)
En logique mathématique, un fragment d'un langage ou d'une théorie logique est un sous-ensemble de ce langage obtenu en lui imposant des restrictions syntaxiques[1]. Par conséquent, les formules bien formées d'un fragment sont un sous-ensemble de celles de la logique originale. Cependant, la sémantique des formules dans le fragment et dans la logique originale coïncide, et ainsi toute formule du fragment peut être exprimée dans la logique d'origine.
La complexité de calcul des tâches telles que la satisfaisabilité ou la vérification de modèle dans un fragment ne peut pas être plus importante que celle de ces mêmes tâches dans la logique d'origine, puisqu'il y a une réduction évidente du premier problème à l'autre. Un problème important de la logique computationnelle est de déterminer des fragments de logiques bien connues telles que la logique du premier ordre qui soient aussi expressifs que possible tout en étant décidables ou bien an ayant une faible complexité[1]. Le domaine de la théorie de la complexité descriptive vise à établir un lien entre la logique et la théorie de la complexité, en identifiant des fragments logiques qui capturent exactement certaines classes de complexité[2].
Notes et références
- Aaron R. Bradley et Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, (ISBN 9783540741138, lire en ligne), p. 70.
- Heinz-Dieter Ebbinghaus et Jörg Flum, Finite Model Theory, Springer, coll. « Perspectives in mathematical logic », , 119–164 p. (ISBN 9783540287889, lire en ligne).