Loading...
Please wait, while we are loading the content...
Similar Documents
Clp() for Automatically Proving Program Properties 1
| Content Provider | Semantic Scholar |
|---|---|
| Author | Hoarau, Sébastien |
| Copyright Year | 1994 |
| Abstract | Various proof methods have been proposed to solve the implication problem , i.e. proving that properties of the form : 8(P ! Q)-where P and Q denote conjunctions of atoms-are logical consequences of logic programs. Nonetheless, it is a commonplace to say that it is still quite a diicult problem. Besides, the advent of the constraint logic programming scheme constitutes not only a major step towards the achievement of ee-cient declarative logic programming systems but also a new eld to explore. By recasting and simplifying the implication problem in the constraint logic programming framework, we deene a generic proof method for the implication problem, which we prove sound from the algebraic point of view. We present four examples using CLP(IN), CLP(RT), CLP(() and RISC-CLP(IR). The logical point of view of the constraint logic programming scheme enables the automation of the proof method. At last, we prove the unsolvability of the implication problem, we point out the origins of the incompleteness of the proposed proof method and we identify two classes of programs for which we give a decision procedure for the implication problem. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.univ-reunion.fr/~gcc/ps/clp5.ps |
| Alternate Webpage(s) | https://www.researchgate.net/profile/Fred_Mesnard/publication/220118006_CLP(chi)_for_Automatically_Proving_Program_Properties/links/02e7e52a2d2888c736000000.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
