Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 5 / Issue 3

available in:   PDF (317 kB) PS (111 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-005-03-0135


Loop-Detection in Hyper-Tableaux by Powerful Model Generation

Frieder Stolzenburg (Universität Koblenz, Institut für Informatik, Germany)

Abstract: Automated reasoning systems often suffer from redundancy: similar parts of derivations are repeated again and again. This leads us to the problem of loop-detection, which clearly is undecidable in general. Nevertheless, we tackle this problem by extending the hyper-tableau calculus as proposed in [Baumgartner, 1998] by generalized terms with exponents, that can be computed by means of computer algebra systems. Although the proposed loop-detection rule is incomplete, the overall calculus remains complete, because loop-detection is only used as an additional, optional mechanism. In summary, this work combines approaches from tableau-based theorem proving, model generation, and integrates computer algebra systems in the theorem proving process.

Keywords: computer algebra systems, hyper-tableau, loop-detection, model generation., terms with exponents