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 Cu_R
• definition of Cu
• definition of 𝒰_ℱ
• definition of 𝔏₁
• definition of 𝔏₂
• definition of check
• definition of mt_Cu
• definition of mt₁

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.

• 2.trs (proof)
• 3.trs (proof)
• 53.trs (proof)
• 55.trs (proof)
• 94.trs (proof)
• 97.trs (proof)

Software

• CSI (version 1.2)
• CeTA (version 2.32)
• HTML versions of the layer system theory files are available here.

Experiments

• result summary
• detailed results