Dear all,
(sIsEmpty works fine, thanks René)
can CPF/CeTA do "split" for relative termination?
"split" can be used as a notational trick, to avoid unlabeling
split for full termination is: SN(D / R-D) && SN(R-D) => SN(R) (application: semantic labeling in the first premise)
http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/1f1ecb1...
I think I want SN(D / R+S) && SN(R-D / S-D) => SN(R/S) (cf. Geser "Relative Termination" (UIB 91-03) Section 3.2)
but I cannot get CeTA to accept this, https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/489
- Johannes.
Dear all,
to "close" this issue:
can CPF/CeTA do "split" for relative termination?
yes it can - and matchbox is using it now.
René explained to me that a design principle in CeTA is (I am paraphrasing) "everything is relative" : a TRS always is a pair (R,S) of sets of (strict and weak) rules, and where this does not make sense, the union R+S is considered.
- Johannes.
termtools@lists.rwth-aachen.de
-
Johannes Waldmann