Loop-Detection in Hyper-Tableaux by Powerful Model Generation
| dc.creator | Stolzenburg,Frieder | |
| dc.date | 1999 | |
| dc.date.accessioned | 2024-02-06T12:49:57Z | |
| dc.date.available | 2024-02-06T12:49:57Z | |
| dc.description | 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. | |
| dc.format | text/html | |
| dc.identifier | https://doi.org/10.3217/jucs-005-03-0135 | |
| dc.identifier | https://lib.jucs.org/article/27543/ | |
| dc.identifier.uri | https://openrepository.mephi.ru/handle/123456789/7532 | |
| dc.language | en | |
| dc.publisher | Journal of Universal Computer Science | |
| dc.relation | info:eu-repo/semantics/altIdentifier/eissn/0948-6968 | |
| dc.relation | info:eu-repo/semantics/altIdentifier/pissn/0948-695X | |
| dc.rights | info:eu-repo/semantics/openAccess | |
| dc.rights | J.UCS License | |
| dc.source | JUCS - Journal of Universal Computer Science 5(3): 135-155 | |
| dc.subject | hyper-tableau | |
| dc.subject | loop-detection | |
| dc.subject | terms with exponents | |
| dc.subject | computer algebra systems | |
| dc.subject | model generation. | |
| dc.title | Loop-Detection in Hyper-Tableaux by Powerful Model Generation | |
| dc.type | Research Article |