Treffer: Solving mixed quantified constraints over a domain based on Real numbers and Herbrand terms

Title:
Solving mixed quantified constraints over a domain based on Real numbers and Herbrand terms
Authors:
GARCIA-DIAZ, Miguel, NIEVA, Susana
Source:
FLOPS 2002 : functional and logic programming (Aizu, 15-17 September 2002)Lecture notes in computer science. :103-118
Publisher Information:
Berlin: Springer, 2002.
Publication Year:
2002
Physical Description:
print, 19 ref
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, Clause Horn, Horn clauses, Langage programmation, Programming language, Lenguaje programación, Logique ordre 1, First order logic, Lógica orden 1, Programmation logique avec contrainte, Constraint logic programming, Programación lógica con restricción, Satisfaction contrainte, Constraint satisfaction, Satisfaccion restricción, Nombre réel, Real number
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Dpto. Sistemas Informáticos y Programación, Universidad Complutense de Madrid, Spain
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=14614872
Rights:
Copyright 2003 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.14614872
Database:
PASCAL Archive

Weitere Informationen

Combining the logic of hereditary Harrop formulas HH with a constraint system, a logic programming language is obtained that extends Horn clauses in two different directions, thus enhancing substantially the expressivity of Prolog. The implementation of this new language requires the ability to test the satisfiability of constraints built up by means of terms and predicates belonging to the domain of the chosen constraint system, and by the connectives and quantifiers usual in first-order logic. In this paper we present a constraint system called RH for a hybrid domain that mixes Herbrand terms and real numbers. It arises when joining the axiomatization of the arithmetic of real numbers and the axiomatization of the algebra of finite trees. We have defined an algorithm to solve certain constraints of this kind. The novelty relies on the combination of two different mechanisms, based on elimination of quantifiers; one used for solving unification and disunification problems, the other used to solve polynomials. This combination provides a procedure to solve RH-constraints in the context of HH with constraints.