Name
Abstract | ||
|---|---|---|
This paper presents a framework for discovering and verifying logic program properties (first order formulas). The aim of this work is the definition of new strategies for transforming logic programs from Horn clauses specifications 171. The property discovery is one of major hurdles in automating the transformation of logic programs. This paper addresses aspects of these related problem. Especially we characterize the manipulated formulas by some syntactical conditions (the notion of eligible formulas), and we present a strategy for synthesizing properties based on contexiual analysis. The system permits verification of the correctness of the transformed programs thanks to the theorem prover. Some deduction rules used by the theorem prover are presented. |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1145/315891.316022 | SAC |
Keywords | DocType | ISBN |
logic program property,theorem prover,theory of computation,first order | Conference | 0-89791-658-1 |
Citations | PageRank | References |
0 | 0.34 | 6 |
Authors | ||
1 | ||