CONFident
Confluence Checker for Conditional Rewrite Systems
Description
- CONFident is a tool for checking the confluence or non-confluence of systems based on rewriting by means of its logical representation.
- CONFident is able to deal with join, oriented, and semi-equational CTRSs.
- CONFident is powered by MU-TERM, infChecker, Prover9 and FORT.
- CONFident participated in the 2021 confluence competition (CoCo) in the CTRS category, winning the first place in the CTRS subcategory (see results).
- CONFident participated in the 2022 confluence competition (CoCo) in the CTRS category, winning the first place in the CTRS subcategory (see results).
- FLoC Olympic Games:
2022: 
Web Interface
- CONFident can be used online through its own web interface.
- CONFident accepts the COPS format for CTRS problems.
Input Program
Select a file to upload, try or paste your code in the following text area:
Results
Related Publications
- S. Lucas, M. Vítores and R. Gutiérrez. Proving and disproving confluence of context-sensitive rewriting.
Journal of Logical and Algebraic Methods in Programming , 126, 100749. Elsevier, 2022. - R. Gutiérrez, S.Lucas and M. Vítores. Confluence of Conditional Rewriting in Logic Form. In: Bojańczyk, M. and Chekuri, C. (eds.)
41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FST&TCS 2021 . LIPIcs, art. 44, 44:1-44:18. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2022. - R. Gutiérrez, S.Lucas and M. Vítores. CONFident at the 2021 Confluence Competition. In: Mimram S., Rocha C. (eds)
10th International Workshop on Confluence, IWC 2021 . 2021. - R. Gutiérrez and S. Lucas. Automatically Proving and Disproving Feasibility Conditions. In: Peltier N., Sofronie-Stokkermans V. (eds)
Automated Reasoning, IJCAR 2020 . LNCS, vol. 12167, 416-435. Springer, 2020. - S.Lucas. Proving semantic properties as first-order satisfiability.
Artificial Intelligence 277, 103174. Elsevier, 2019.