A Resolution Principle for a Logic with Restricted Quantifiers

1991
ISBN: 978-3-540-55034-1
Verlag: Springer Berlin Heidelberg

Buch, Englisch, Band 568, 120 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 213 g

Reihe: Lecture Notes in Computer Science

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.

Zielgruppe

Research

Autoren/Hrsg.

Bürckert, Hans-Jürgen

Fachgebiete

• Mathematik | Informatik EDV | Informatik Informatik Mathematik für Informatiker
• Mathematik | Informatik EDV | Informatik Informatik Künstliche Intelligenz Wissensbasierte Systeme, Expertensysteme
• Mathematik | Informatik Mathematik Mathematik Allgemein Grundlagen der Mathematik
• Mathematik | Informatik EDV | Informatik Informatik Logik, formale Sprachen, Automaten
• Technische Wissenschaften Elektronik | Nachrichtentechnik Elektronik Robotik

Inhaltsverzeichnis

Preliminaries.- Unification.- A logic with restricted quantifiers.- Equational constraint theories.- Conclusion.