Result: Quantifier elimination for constraint logic programming

Title:
Quantifier elimination for constraint logic programming
Authors:
STURM, Thomas
Source:
CASC 2005 : computer algebra in scientific computing (Kalamata, 12-16 September 2005)Lecture notes in computer science. :416-430
Publisher Information:
Berlin: Springer, 2005.
Publication Year:
2005
Physical Description:
print, 23 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Mathematics, Mathématiques, 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, Algorithmique. Calculabilité. Arithmétique ordinateur, Algorithmics. Computability. Computer arithmetics, Algèbre, Algebra, Arithmétique Presburger, Presburger arithmetic, Aritmético Presburger, Calcul formel, Computer algebra, Cálculo formal, Calcul propositionnel, Propositional calculus, Cálculo proposicional, Congruence, Congruencia, Faisabilité, Feasibility, Practicabilidad, Nombre complexe, Complex number, Número complejo, Ordre linéaire, Linear ordering, Orden lineal, Programmation logique avec contrainte, Constraint logic programming, Programación lógica con restricción, Relation ordre, Ordering, Relación orden, Satisfaction contrainte, Constraint satisfaction, Satisfaccion restricción, Elimination quantificateur, Quantifier elimination, Eliminación cuentificador
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
FMI, Universität Passau, 94030 Passau, Germany
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=17115588
Rights:
Copyright 2005 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.17115588
Database:
PASCAL Archive

Further Information

We present an extension of constraint logic programming, where the admissible constraints are arbitrary first-order formulas over various domains: real numbers with ordering, linear constraints over p-adic numbers, complex numbers, linear constraints over the integers with ordering and congruences (parametric Presburger Arithmetic), quantified propositional calculus (parametric QSAT), term algebras. Our arithmetic is always exact. For R are C there are no restrictions on the polynomial degree of admissible constraints. Constraint solving is realized by effective quantifier elimination. We have implemented our methods in our system CLP(RL). A number of computation examples with CLP(RL) are given in order to illustrate the conceptual generalizations provided by our approach and to demonstrate its feasibility.