Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00150707
Contributor : Sylvain Soliman <>
Submitted on : Thursday, May 31, 2007 - 2:29:51 PM
Last modification on : Thursday, March 5, 2020 - 6:24:28 PM

Identifiers

  • 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. ⟨inria-00150707⟩

Share

Metrics

Record views

130