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

Inès Mouakher; Francis Alexandre; Khaled Bsaïes

inria-00000070, version 1

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

Inès Mouakher ¹, Francis Alexandre () ², Khaled Bsaïes ¹

Premières Journées Francophones de Programmation par Contraintes - JFPC'2005 (2005) 179-188

Abstract: 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.

1: Faculté des Sciences de Tunis (FST)
Faculté des Sciences de Tunis
2: DEDALE (LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)

inria-00000070, version 1
http://hal.inria.fr/inria-00000070
oai:hal.inria.fr:inria-00000070
From: Christine Solnon <>
Submitted on: Thursday, 26 May 2005 11:10:48
Updated on: Wednesday, 12 July 2006 10:49:05

See detailed view

Associated documents

PS :

PDF :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="inria-00000070"><analytic>
<author><persName><forename>Inès</forename><surname>Mouakher</surname></persName>
<affiliation>
<orgName type="laboratory">FST</orgName>
<orgName type="team">Faculté des Sciences de Tunis</orgName>
<country>TN</country>
<orgName type="institution">Faculté des Sciences de Tunis</orgName>
</affiliation>
</author>
<author><persName><forename>Francis</forename><surname>Alexandre</surname></persName>
<affiliation>
<orgName type="laboratory">LORIA</orgName>
<orgName type="team">DEDALE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Khaled</forename><surname>Bsaïes</surname></persName>
<affiliation>
<orgName type="laboratory">FST</orgName>
<orgName type="team">Faculté des Sciences de Tunis</orgName>
<country>TN</country>
<orgName type="institution">Faculté des Sciences de Tunis</orgName>
</affiliation>
</author>
<title type="main" level="a">Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives</title></analytic><monogr><meeting>Premières Journées Francophones de Programmation par Contraintes - JFPC'2005</meeting><imprint><publisher>Université d'Artois</publisher><pubPlace><settlement>Lens</settlement><country>France</country></pubPlace><biblScope type="publicationDate">2005-06-08</biblScope><biblScope type="pp">179-188</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00000070</idno><idno type="HALFile">http://hal.inria.fr/inria-00000070/PDF/30.pdf</idno></biblStruct>
</listBibl>
</listBibl>