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.)
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.