MU-TERM GTRS

Termination Tool for Generalized Term Rewrite Systems


Description

  • MU-TERM GTRS is a tool which can be used to analyze termination of Generalized Term Rewriting Systems (GTRSs).
  • MU-TERM GTRS is powered by the theorem prover Prover9 and the model generators Mace4 and AGES. AGES is powered by the SMT solver Barcelogic.

Web Interface

  • MU-TERM GTRS can be used online through his own web interface.
  • MU-TERM GTRS accepts an enrichment version of the TPDB format, allowing predicates.

Input Program

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

Select timeout in seconds (1 <= timeout <= 300):

Output

     
            

            

            

              
Benchmarks

      
CSR + CTRS Benchmarks - Timeout 240s (see details)


      

        
        

        Termination Tool
        YES
        NO
        MAYBE
        

        

        MU-TERM 6
        186/225
        3/225
        36/225
        

        

        MU-TERM GTRS
        133/225
        29/225
        63/225
        

        
      

            

      

      

      

      

            

              
Bibliography

                
    
                
  • Salvador Lucas. Termination of Generalized Term Rewriting Systems. In Jakob Rehof, editor, Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, Tallinn, Estonia, July 10-13. Leibniz International Proceedings in Informatics (LIPIcs), volume 299, paper 29, pages 1-18, 2024. doi: 10.4230/LIPIcs.FSCD.2024.29
    • 
                
  • Salvador Lucas. Local confluence of conditional and generalized term rewriting systems. Journal of Logical and Algebraic Methods in Programming 299, paper 100926, pages 1-23, 2024. doi: 10.1016/j.jlamp.2023.100926
    • 
                

                

            

            

            
Team/Contact

              
Members:
              

              

            

            

              
Financial Support

              
Supported by MCIN/AEI/10.13039/501100011033 and by “ERDF A way of making Europe” (PID2021-122830OB-C42 and PID2021-122830OB-C44) and by the grant CIPROM/2022/6 funded by Generalitat Valenciana