Layer Systems for Confluence — Formalized
About
This website contains examples and experimental results for the paper Layer Systems for Confluence — Formalized to be presented at ICTAC 2018.
List of definitions
The official version of the paper has no links inside formulas. We provide links to the formalized definitions for selected notation here.- definition of 𝒯
- definition of 𝒞
- definition of 𝔏α
- definition of 𝔏
- definition of mtα
- definition of ⊵
- defintion of ℛα
- definition of CuR
- definition of Cu
- definition of 𝒰ℱ
- definition of 𝔏1
- definition of 𝔏2
- definition of check
- definition of mtCu
- definition of mt1
Example proofs
- confluent example 1
# csi -e -cpf -s CERT_ALL CLe.trs > CLe.xml YES # ceta CLe.xml CERTIFIED
files: CLe.trs (input) CLe.xml (proof) - confluent example 2 (cf. Cops)
# csi -e -cpf -s CERT_ALL cops3.trs > cops3.xml YES # ceta cops3.xml CERTIFIED
files: cops3.trs (input) cops3.xml (proof) - non-confluent example
# csi -e -cpf -s CERT_ALL ncr.trs > ncr.xml NO # ceta ncr.xml CERTIFIED
files: ncr.trs (input) ncr.xml (proof)
Confluence of the following 6 TRSs (from Cops) can be certified thanks to persistent decomposition.
Software
- CSI (version 1.2)
- CeTA (version 2.32)
- HTML versions of the layer system theory files are available here.