Hi Johannes,

I think you can do that: here is the IsaFoR/CeTA-code that checks correct application

"check_rule_preserving fcs rs' rule ≡ ( check ((Bex (set rs') (instance_rule rule)) ∨ (∀C∈set fcs. Bex (set rs') (instance_rule (C⟨fst rule⟩, C⟨snd rule⟩)))) (showsl_lit (STR ''the rule '') ∘ showsl_rule rule ∘ showsl_lit (STR '' is neither contained in the resulting set of rules nor closed under all flat contexts⏎''))

so, for each “rule" in R, it is tested whether that rule is in R’, or the full context-closure of that rule is in R’ (modulo variable-renamings via “instance_rule”)

Since I did not change the code of FCCs for CeTA 2.46 and CeTA 3.1, this should work, but please test beforehand.

Best, René

Am 17.06.2024 um 14:42 schrieb Johannes Waldmann johannes.waldmann@htwk-leipzig.de:

Dear all,

can I express in CPF (for Ceta-2) that I want to apply "flat context closure" to a subset of rules only?

specifically, I want this for rules with empty lhs or rhs, as it seems to increase the power of matrix interpretations. (as shown by Aprove in TC 23).

I am looking at http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/8250228... but the example seems to close all rules.

I guess I can indeed context-close all rules uniformly, and use the same interpretation, to remove the same rules. But perhaps I want other methods that refer to the original rules.

Well it's a bit late anyway.

• J.

---

Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de