About this book
Introduction
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.
Keywords
Beschränkte Quantoren Deduction and Theorem Proving Deduktion und Beweisen Extension Knowledge Representation Logic Programming Logisches Programmieren Mathematical Logic Mathematische Logik Resolution Restricted Quantifiers Wissens-Darstellung calculus logic sets
Bibliographic information