Details

Autor(en) / Beteiligte

• Moser, Max
• Ibens, Ortrun
• Letz, Reinhold
• Steinbach, Joachim
• Goller, Christoph
• Schumann, Johann
• Mayr, Klaus

Titel

SETHEO and E-SETHEO - The CADE-13 Systems

Ist Teil von

• Journal of automated reasoning, 1997-04, Vol.18 (2), p.237

Ort / Verlag

Dordrecht: Springer Nature B.V

Erscheinungsjahr

1997

Quelle

SpringerLINK Contemporary (Konsortium Baden-Württemberg)

Beschreibungen/Notizen

• The model elimination theorem prover SETHEO (version V3.3) and its equational extension E-SETHEO are presented. SETHEO employs sophisticated mechanisms of subgoal selection, elaborate iterative deepening techniques, and local failure caching methods. Its equational counterpart E-SETHEO transforms formulae containing equality (using a variant of Brand's modification method) and processes the output with the standard SETHEO system. This article gives an overview of the theoretical background, the system architecture, and the performance of both systems.[PUBLICATION ABSTRACT]