EVA STAR Trefferanzeige

Volltext Volltext.pdf1.pdf (137 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-AAA216964
Titel Incremental theory reasoning methods for semantic tableaux.
Autor Beckert, Bernhard
Pape, Christian
Institution Fakultät für Informatik (INFORMATIK)
Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Dokumenttyp Buch
Jahr 1996
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,2.)
Abstract
Theory reasoning is an important technique for increasing the
efficiency of automated deduction systems. In this paper we present
incremental theory reasoning, a method that improves the interaction
between the foreground reasoner and the background (theory) reasoner
and, thus, the efficiency of the combined system. The use of
incremental theory reasoning in free variable semantic tableaux
and the cost reduction that can be achieved are discussed; as an
example, completion-based equality reasoning is presented, including
experimental data obtained using an implementation.