Skip to Main content Skip to Navigation
Conference papers

Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives

Résumé : L'objectif général de ce travail est de prouver les propriétés des programmes logiques (ensemble de clauses de Horn). Ces propriétés sont des formules de la forme A <-- B où A et B sont des conjonctions d'atomes. Nous disposons d'un ensemble de règles de déductions tels que le pliage, le dépliage et la simplification. La preuve consiste à appliquer l'une de ces règles sur la formule à prouver jusqu'à aboutir à un ensemble de formules triviales. Une étape essentielle dans le processus de la preuve est la réussite du pliage qui peut être vue comme l'application d'une hypothèse de récurrence dans une preuve inductive. Nous proposons des stratégies pour automatiser partiellement le processus de preuve en nous basant sur une analyse statique des formules et des programmes.
Complete list of metadata

https://hal.inria.fr/inria-00000070
Contributor : Christine Solnon <>
Submitted on : Thursday, May 26, 2005 - 11:10:48 AM
Last modification on : Friday, February 26, 2021 - 3:28:07 PM
Long-term archiving on: : Thursday, April 1, 2010 - 9:33:13 PM

Files

Identifiers

  • HAL Id : inria-00000070, version 1

Collections

Citation

Inès Mouakher, Francis Alexandre, Khaled Bsaïes. Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives. Premières Journées Francophones de Programmation par Contraintes - JFPC'2005, CRIL - CNRS FRE 2499, Jun 2005, Lens/France, pp.179-188. ⟨inria-00000070⟩

Share

Metrics

Record views

117

Files downloads

155