This monograph presents foundations for a constrained
logic scheme treating constraints as a very general form of
restricted quantifiers. The constraints - or quantifier
restrictions - are taken from a general constraint system
consisting of constraint theory and a set of distinguished
constraints.
The book provides a calculus for this constrained logic
based on a generalization of Robinson's resolution
principle. Technically, the unification procedure of the
resolution rule is replaced by suitable constraint-solving
methods. The calculus is proven sound and complete for the
refutation of sets of constrained clauses. Using a new and
elegant generalization of the notion ofa ground instance,
the proof technique is a straightforward adaptation of the
classical proof technique.
The author demonstrates that the constrained logic scheme
can be instantiated by well-known sorted logics or
equational theories and also by extensions of predicate
logics with general equational constraints or concept
description languages.
Produkteigenschaften
- Artikelnummer: 9783540550341
- Medium: Buch
- ISBN: 978-3-540-55034-1
- Verlag: Springer Berlin Heidelberg
- Erscheinungstermin: 11.12.1991
- Sprache(n): Englisch
- Auflage: 1991
- Serie: Lecture Notes in Computer Science
- Produktform: Kartoniert
- Gewicht: 213 g
- Seiten: 120
- Format (B x H x T): 155 x 235 x 8 mm
- Ausgabetyp: Kein, Unbekannt