Preuves, réfutations et contre-modèles dans des logiques intuitionnistes
Résumé
Logics can be used as powerful tools for specifying computer systems and proving the soundness of their implementations with respect to these specifications. In the field of substructural logics, we develop tools and methods for automated deduction and counter-model generation. These logics involve the notion of resource : at the level of proof-search, the management of resources enables more efficient procedures : at the semantic level, resource models provide sound and complete interpretations. We develop a link between the syntactic notion of refutation and the semantic notion of counter-model. We deduce methods for proving the finite model property and algorithms for implementation of a proof-search procedure, based on a fine management of resources. In intuitionistic linear logic, resource based models constitute the core of an elegant proof of the finite model property. Furthermore, we establish a link between resource models and Petri net based models, from which we improve the proeceding partial completness results.
Les logiques sont de puissants outils qui permettent la spécification de systèmes informatiques et la preuve de l'adéquation de leurs implantations avec ces spécifications. Dans le cadre des logiques sous-structurelles, nous mettons en place des outils de démonstration automatique et de construction de contre-modèles. Ces logiques intègrent la notion de ressource ; au niveau de la recherche de preuve, la gestion des ressources permet la mise en place de procédures plus efficaces ; au niveau de l'interprétation sémantique, la notion de ressource permet de construire des modèles fidèles et complets. Nous établissons un lien entre la notion syntaxique de réfutation et la notion sémantique de contre-modèle. Nous en déduisons des méthodes de démonstration de la propriété des modèles finis ainsi que des algorithmes de construction de contre-modèles. En logique intuitionniste propositionnelle, la gestion fine de ressources permet d'en déduire une implantation efficace de la recherche de preuves. En logique intuitionniste linéaire, les modèles à base de ressources permettent une preuve élégante de la propriété des modèles finis. Nous établissons un lien entre la sémantique des ressources et la sémantique à base de réseaux de Petri, ce qui permet de raffiner les résultats de complétude partiels connus jusqu'alors.