KIT | KIT-Bibliothek | Impressum | Datenschutz

Incremental theory reasoning methods for semantic tableaux

Beckert, Bernhard ORCID iD icon; 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.

Volltext §
DOI: 10.5445/IR/21696
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1996
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA216964
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