Proof Transformations from Search-Oriented into Interaction-Oriented Tableau Calculi
| dc.creator | Stenz,Gernot | |
| dc.creator | Ahrendt,Wolfgang | |
| dc.creator | Beckert,Bernhard | |
| dc.date | 1999 | |
| dc.date.accessioned | 2024-02-06T12:49:57Z | |
| dc.date.available | 2024-02-06T12:49:57Z | |
| dc.description | Logic calculi, and Gentzen-type calculi in particular, can be categorised into two types: search-oriented and interaction-oriented calculi. Both these types have certain inherent characteristics stemming from the purpose for which they are designed. In this paper, we give a general characterisation of the two types and present two calculi that are typical representatives of their respective class. We introduce a method for transforming proofs in the search-oriented calculus into proofs in the interaction-oriented calculus, and we demonstrate that the difficulties arising with devising such a transformation do not pertain to the specific calculi we have chosen as examples but are general. We also give examples for the application of our transformation procedure. | |
| dc.format | text/html | |
| dc.identifier | https://doi.org/10.3217/jucs-005-03-0113 | |
| dc.identifier | https://lib.jucs.org/article/27542/ | |
| dc.identifier.uri | https://openrepository.mephi.ru/handle/123456789/7531 | |
| 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): 113-134 | |
| dc.subject | automated deduction | |
| dc.subject | tableau calculi | |
| dc.subject | proof transformation | |
| dc.subject | proof presentation | |
| dc.subject | proof search | |
| dc.title | Proof Transformations from Search-Oriented into Interaction-Oriented Tableau Calculi | |
| dc.type | Research Article |