Craciunescu, Sorin (2004) Proving the Equivalence of Logic Programs. PhD thesis INRIA, INRIA, EP/X p.170.
Full text not available from this repository. |
|
Alternative Locations: http://www.imprimerie.polytechnique.fr/Theses/Files/Craciunescu.pdf
Abstract
The goal of this work is to present a formal system that can be used to prove the success equivalence of logic programs.
By proving success equivalence one can prove that a program representing the specification and another one representing the implementation are equivalent.
This can be done by proving that the set of successes of each program is included in the corresponding set of the other one.
The language studied is CLPforall which is the Constraint Logic Programming (CLP) language to which the universal quantifier was added.
The set of finite success of a program is defined by the finite success semantics of the language.
We define also the set of infinite success of a program by extending the definitions for finite success to take into account infinite (non-terminating) computations.
This gives the infinite success semantics of the language.
We prove that the sets of finite and infinite successes are given by the least and greatest fixed point of the same operator.
In order to prove success inclusion we propose a proof system based of the first-order classical logic.
The rules for logical operators and quantifiers are the same as in first-order logic.
In order to reason about recursively defined predicates we add an induction rule and we prove the correctness of the system under certain conditions.
This constitutes the main contribution of this work.
The proof of other properties can be reduced to the proof of success inclusion.
The same proof system can be used to prove infinite success inclusion by replacing the induction rule with a coinduction rule.
We prove the correctness of the system under conditions analogous to those for finite successes.
We also show that the two systems are equivalent under some conditions related to the existence of negated constraints.
The implementation of a proof assistant written in Prolog is presented.
The software assists the user in building proof and has a simple but effective proof-search procedure that reduces the user's work.
| Item Type: | PhD Thesis (PhD) |
|---|---|
| Thesis Supervisor: | Fages, François |
| Date: | March 2004 |
| Board of examiners: | Dowek, Gilles and Ferrand, Gérrard and Miller, Dale and Fages, François and Jaume, Mathieu |
| Ecole Doctorale: | ED 447 ECOLE DOCTORALE DE L'ECOLE POLYTECHNIQUE |
| Discipline: | INRIA |
| Collection (Fonds): | EP/X |
| Institution: | EP/X |
| Department: | INRIA |
| Subjects: | 2. Information and Communication Sciences and Technologies |
| Uncontrolled Keywords: | Formal verification, Equivalence proofs, First-order logic, Induction, Coinduction, Infinite success, Logic languages, Constraint programming, Clp., Vérification formelle, Preuves déquivalence, Logique du premier ordre, Induction, Coinduction, Succès infinis, Langages logiques, Programmation par contraintes, Clp. |
| ID Code: | 864 |
|---|---|
| Deposited By: | Nadine Garnier |
| Deposited On: | 13 October 2004 |
Repository Staff Only: edit this item