Treffer: Proving properties of constraint logic programs by eliminating existential variables

Title:
Proving properties of constraint logic programs by eliminating existential variables
Authors:
PETTOROSSI, Alberto, PROIETTI, Maurizio, SENNI, Valerio
Source:
Logic programming (22nd international conference, ICLP 2006)0ICLP 2006. :179-195
Publisher Information:
Berlin: Springer, 2006.
Publication Year:
2006
Physical Description:
print, 20 ref 1
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Fonctions logiques, booléennes et de commutation, Logical, boolean and switching functions, Corps, Body, Cuerpo, Modélisation, Modeling, Modelización, Programmation logique avec contrainte, Constraint logic programming, Programación lógica con restricción, Programmation logique, Logical programming, Programación lógica, Tête, Head, Cabeza
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
DISP, University of Roma Tor Vergata, Via del Politecnico 1, 00133 Roma, Italy
IASI-CNR, Viale Manzoni 30, 00185 Roma, Italy
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=19104701
Rights:
Copyright 2007 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.19104701
Database:
PASCAL Archive

Weitere Informationen

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.