KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo
URN: urn:nbn:de:swb:90-AAA216964

Incremental theory reasoning methods for semantic tableaux

Beckert, Bernhard; Pape, Christian


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.

Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Jahr 1996
Sprache Englisch
Identifikator KITopen ID: 21696
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,2.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page