Back to Search
Start Over
CLP(χ) for automatically proving program properties1An earlier version of this paper was presented at the workshop 'Frontiers of Combining Systems', Munich, March 1996.1
- Source :
- The Journal of Logic Programming. (1-3):77-93
- Publisher :
- Elsevier Science B.V.
-
Abstract
- Various proof methods have been proposed to solve the implication problem, i.e. proving that properties of the form: ∀( P → Q ) – where P and Q denote conjunctions of atoms – are logical consequences of logic programs. Nonetheless, it is commonplace to say that it is still quite a difficult problem. Besides, the advent of the constraint logic programming scheme constitutes not only a major step towards the achievement of efficient declarative logic programming systems but also a new field to explore. By recasting and simplifying the implication problem in the constraint logic programming (CLP) framework, we define a generic proof method for the implication problem, which we prove sound from the algebraic point of view. We present four examples using CLP( N ), CLP( RT ), CLP( Σ ∗ ) and RISC-CLP( R ). 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.
- Subjects :
- Concurrent constraint logic programming
Discrete mathematics
Constraint logic programming
Horn clause
Functional logic programming
Logic
Proof theory
Algebra
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Satisfiability modulo theories
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Constraint programming
Verifying and reasoning about programs
Logic programming
Mathematics
Subjects
Details
- Language :
- English
- ISSN :
- 07431066
- Issue :
- 1-3
- Database :
- OpenAIRE
- Journal :
- The Journal of Logic Programming
- Accession number :
- edsair.doi.dedup.....0565103989348ca507088a779f06a952
- Full Text :
- https://doi.org/10.1016/S0743-1066(98)10004-3