infChecker

Description

infChecker is a tool which can be used to verify infeasibility conditions of variants of Term Rewriting Systems (TRSs).
infChecker is powered by the theorem prover Prover9 and the model generators Mace4 and AGES. AGES is powered by the SMT solver Barcelogic.
infChecker participated in the 2019 confluence competition (CoCo) in the INF category (see results), in the 2020 confluence competition (CoCo) in the INF category (see results), in the 2021 confluence competition (CoCo) in the INF category (see results) and in the 2021 confluence competition (CoCo) in the INF category (see results). Currently, infChecker is the most powerful tool for proving and disproving infeasibility.
FLoC Olympic Games:
2022:

infChecker can be used online through his own web interface.
infChecker accepts the inlined COPS format for infeasibility problems.
infChecker accepts context-sensitive (CS) rewriting systems by adding replacing restrictions using the TPDB sintax.
infChecker also accepts the following relations on conditions:
- One rewriting step (->).
- One CS-rewriting step (\->).
- Zero or one rewriting step (->=).
- Zero or one CS-rewriting step (\->=).
- Zero or more rewriting steps (->*).
- Zero or more CS-rewriting steps (\->*).
- One or more rewriting steps (->+).
- One or more CS-rewriting steps (\->+).
- Subterm (|>=) and strict subterm (|>).
- Joinability (->*<-).
- CS-joinability (\->*<-/).
- One convertibility step (<-->).
- One CS-convertivility step (<-/\->).
- Zero or more convertibility steps (<-->*).
- Zero or more CS-convertibility steps (<-/\->*).

Select a file to upload, try or paste your code un the following text area:

R. Gutiérrez, S.Lucas and M. Vítores. infChecker 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.
S.Lucas. Proving Program Properties as First-Order Satisfiability. In: Mesnard F., Stuckey P. (eds) Logic-Based Program Synthesis and Transformation, LOPSTR 2018. LNCS, vol. 11408, 3-21. Springer, 2019.
S. Lucas and R. Gutiérrez. Use of Logical Models for Proving Infeasibility in Term Rewriting. Information Processing Letters 136, 90-95, Elsevier, 2018.
S. Lucas and R. Gutiérrez. Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories. Journal of Automated Reasoning 60, 465-501. Springer, 2018.
S.Lucas. Analysis of Rewriting-Based Systems as First-order Theories. In: Fioravanti F., Gallagher J. (eds) Logic-Based Program Synthesis and Transformation, LOPSTR 2017. LNCS, vol. 10855, 180-197. Springer, 2018.