Les contraintes de la logique

Résumé : La résolution de contraintes est un problème qui se pose naturellement quand on cherche à étendre des algorithmes de démonstration automatique, comme la résolution ou les tableaux, à des logiques dans lesquelles une théorie est définie par des axiomes et des règles de calcul. Vouloir raisonner et calculer oblige donc à résoudre. Cependant, quand les règles de calcul s'appliquent, non seulement à des termes, mais aussi à des formules, résoudre des contraintes ne suffit plus et des opérations similaires doivent être utilisées à d'autres étapes de la recherche des démonstrations. Les algorithmes universels de résolution de contraintes, comme la surréduction, ont souvent été remplacés par des algorithmes spécialisés beaucoup plus efficaces. On s'interrogera dans cet exposé sur la possibilité d'opérer un remplacement similaire pour ces opérations.
Type de document :
Communication dans un congrès
Troisièmes Journées Francophones de Programmation par Contraintes (JFPC07), Jun 2007, INRIA, Domaine de Voluceau, Rocquencourt, Yvelines France, 2007, JFPC07
Liste complète des métadonnées

https://hal.inria.fr/inria-00150707
Contributeur : Sylvain Soliman <>
Soumis le : jeudi 31 mai 2007 - 14:29:51
Dernière modification le : jeudi 10 mai 2018 - 02:06:54

Identifiants

  • HAL Id : inria-00150707, version 1

Collections

Citation

Gilles Dowek. Les contraintes de la logique. Troisièmes Journées Francophones de Programmation par Contraintes (JFPC07), Jun 2007, INRIA, Domaine de Voluceau, Rocquencourt, Yvelines France, 2007, JFPC07. 〈inria-00150707〉

Partager

Métriques

Consultations de la notice

89