We propose a method for proving first order properties of constraint logic programs which manipulate finite lists of real numbers. Constraints are linear equations and inequations over reals. Our method consists in converting any given first order formula into a stratified constraint logic program and then applying a suitable unfold/fold transformation strategy that preserves the perfect model. Our strategy is based on the elimination of existential variables, that is, variables which occur in the body of a clause and not in its head. Since, in general, the first order properties of the class of programs we consider are undecidable, our strategy is necessarily incomplete. However, experiments show that it is powerful enough to prove several non-trivial program properties.

Pettorossi, A., Proietti, M., Senni, V. (2006). Proving properties of constraint logic programs by eliminating existential variables. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp.179-195). Berlin : Springer-Verlag.

### Proving properties of constraint logic programs by eliminating existential variables

#### Abstract

We propose a method for proving first order properties of constraint logic programs which manipulate finite lists of real numbers. Constraints are linear equations and inequations over reals. Our method consists in converting any given first order formula into a stratified constraint logic program and then applying a suitable unfold/fold transformation strategy that preserves the perfect model. Our strategy is based on the elimination of existential variables, that is, variables which occur in the body of a clause and not in its head. Since, in general, the first order properties of the class of programs we consider are undecidable, our strategy is necessarily incomplete. However, experiments show that it is powerful enough to prove several non-trivial program properties.
##### Scheda breve Scheda completa Scheda completa (DC)
22nd International Conference on Logic Programming, ICLP 2006
Seattle, WA
2006
Rilevanza internazionale
contributo
2006
Settore ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
English
Constraint theory; Linear equations; Mathematical models; Mathematical transformations; Constraint logic programs; Fold transformation strategy; Logic programming
Intervento a convegno
Pettorossi, A., Proietti, M., Senni, V. (2006). Proving properties of constraint logic programs by eliminating existential variables. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp.179-195). Berlin : Springer-Verlag.
Pettorossi, A; Proietti, M; Senni, V
File in questo prodotto:
File
PetProSen_ICLP06long.pdf

accesso aperto

Dimensione 263.34 kB
Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/2108/41691`