Subcategories
CSI
CSI is an automatic confluence prover for first-order rewrite systems. An extension to higher-order pattern rewrite systems is described here.
News
- July 2021: Version 1.2.5 released. (CoCo 2021 version; adds outside-closure criterion)
- June 2020: Version 1.2.4 released. (CoCo 2020 version; adds upside-parallel-closure criterion)
- April 2019: Version 1.2.3 released. (CoCo 2019 version; adds UNC for shallow systems)
- December 2018: Version 1.2.2 released. (right-reducibility for NFP; improved SRS support for CR)
- June 2018: Version 1.2.1 released. (CoCo 2018 version; adds UNC for linear shallow systems)
- January 2018: Version 1.2 released. (adds certification for persistent decomposition).
- September 2017: Version 1.1 released. (CoCo 2017).
- June 2017: Version 1.0.1 released. (improved UNR check for ground TRSs).
- February 2017: Version 1.0 released (experiments).
- September 2016: Version 0.6 released (CoCo 2016).
- July 2015: Version 0.5.1 released (CoCo 2015).
- February 2015: Version 0.5 released (certified rule labeling; removal and addition of redundant rules).
- January 2014: Version 0.4.1 released (improved strategy for non-left-linear TRSs).
- November 2013: Version 0.4 released (improved incremental labeling).
- July 2013: Version 0.3 released (CoCo 2013).
- May 2012: Version 0.2 released (CoCo 2012).
- February 2011: Version 0.1 released (experiments).
Download
Use the web interface or statically linked precompiled binaries for Linux (32 bit, 64 bit) if you do not want to build CSI on your own.
You can also download the source. The current version is 1.2.5. To compile
- download and extract the archive
- follow the instructions in README
- type make
- type ./csi.sh <file>
Documents
- Julian Nagele, Bertram Felgenhauer, Aart Middeldorp
CSI: New Evidence – A Progress Report
Proc. 26th International Conference on Automated Deduction
LNCS (LNAI) 10395, pp. 385 – 397, 2017. - Bertram Felgenhauer
Efficiently Deciding Uniqueness of Normal Forms and Unique Normalization for Ground TRSs
Proc. 5th International Workshop on Confluence, pp. 16 – 20, 2016. - Julian Nagele, Aart Middeldorp
Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
Proc. 7th International Conference on Interactive Theorem Proving, LNCS 9807, pp. 290 – 306, 2016. - Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules
Proc. 26th International Conference on Rewriting Techniques and Applications, LIPIcs 36, pp. 257 – 268, 2015. - Julian Nagele, Harald Zankl
Certified Rule Labeling
Proc. 26th International Conference on Rewriting Techniques and Applications, LIPIcs 36, pp. 269 – 284, 2015. - Bertram Felgenhauer
Confluence for Term Rewriting: Theory and Automation
PhD thesis, University of Innsbruck, 2015. - Bertram Felgenhauer, Aart Middeldorp, Harald Zankl, Vincent van Oostrom
Layer Systems for Proving Confluence
ACM Transactions on Computational Logic 16(2:14), pp. 1 – 32, 2015. - Harald Zankl, Bertram Felgenhauer, Aart Middeldorp
Labelings for Decreasing Diagrams
Journal of Automated Reasoning 54(2), pp. 101 – 133, 2015. - Harald Zankl
Challenges in Automation of Rewriting
Habilitation thesis, University of Innsbruck, 2014. - Bertram Felgenhauer
Rule Labeling for Confluence of Left-Linear Term Rewrite Systems
Proc. 2nd International Workshop on Confluence, pp. 23 – 27, 2016. - Bertram Felgenhauer
Deciding Confluence of Ground Term Rewrite Systems in Cubic Time
Proc. 23rd International Conference on Rewriting Techniques and Applications, LIPIcs 15, pp. 165 – 175, 2012. - Bertram Felgenhauer, Harald Zankl, Aart Middeldorp
Layer Systems for Proving Confluence
Proc. 30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs 13, pp. 288 – 299, 2011. - Harald Zankl, Bertram Felgenhauer, Aart Middeldorp
CSI – A Confluence Tool (system description)
Proc. 23rd International Conference on Automated Deduction
LNCS (LNAI) 6803, pp. 499 – 505, 2011. - Harald Zankl, Bertram Felgenhauer, Aart Middeldorp
Labelings for Decreasing Diagrams
Proc. 22nd International Conference on Rewriting Techniques and Applications
LIPIcs 10, pp. 277 – 392, 2011.
Contact
The main developers are (in alphabetical order) Bertram Felgenhauer, Aart Middeldorp, Julian Nagele, and Harald Zankl. For any questions or feedback please write to
Support
The development of CSI is supported by FWF (Austrian Science Fund) projects P22467 and P27528.