In this paper, we introduce a method for proving universal termination of constraint logic programs by strictly extending the approach of Apt and Pedreschi [1]. Taking into account a generic constraint domain instead of the standard Herbrand univers, acceptable (CLP) programs are defined. We prove correctness and completeness of the method w.r.t. the leftmost selection rule for the class of ideal constraint systems, including CLP(R lin ), CLP(RT), and CLP(FT) among the others. Moreover, we investigate the problems arising in extending those results to non-ideal constraint system, by specifically designing sufficient conditions for termination of CLP(R) programs.
Termination of Constraint Logic Programs
RUGGIERI, SALVATORE
1997-01-01
Abstract
In this paper, we introduce a method for proving universal termination of constraint logic programs by strictly extending the approach of Apt and Pedreschi [1]. Taking into account a generic constraint domain instead of the standard Herbrand univers, acceptable (CLP) programs are defined. We prove correctness and completeness of the method w.r.t. the leftmost selection rule for the class of ideal constraint systems, including CLP(R lin ), CLP(RT), and CLP(FT) among the others. Moreover, we investigate the problems arising in extending those results to non-ideal constraint system, by specifically designing sufficient conditions for termination of CLP(R) programs.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
