can CeTA infer relative termination from absolute termination?
Dear all, for proving relative termination SN(R/S), a very crude method is to infer it from SN(R \cup S). Does the CPF format (the CeTA verifier) have a provision for that? - Johannes. NB: crude, but powerful, on current SRS_Relative benchmarks, see our WST contribution ...
Dear Johannes, yes, this is already supported according to CPF: there is the sIsEmpty-proof which takes a termination proof for a single TRS (R union S) as argument. doku: state that the R/S is relative terminating by termination of R since S has no rules. (or more generally: prove termination of R union S.) Best, René
Am 09.08.2023 um 09:33 schrieb Johannes Waldmann <johannes.waldmann@htwk-leipzig.de>:
Dear all,
for proving relative termination SN(R/S), a very crude method is to infer it from SN(R \cup S).
Does the CPF format (the CeTA verifier) have a provision for that?
- Johannes.
NB: crude, but powerful, on current SRS_Relative benchmarks, see our WST contribution ... _______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
participants (2)
-
Johannes Waldmann -
Thiemann, René