[Termtools] Outermost Category

Fri Oct 31 08:30:26 CET 2008

Dear all,

Jörg wrote:

> up to now there is no outermost rewriting category.
>
> I think it would be useful to have such a category
> this year since there has been a lot of development:
> - Cariboo has been improved
> - Matthias Raffelsieper and Hans Zantema developed a transformation  
> to TRS
> - Rene Thiemann developed a transformation to innermost termination
> - and I have developed a transformation to context sensitive TRS
>
> We should include outermost to have an objective comparison of the  
> tools.

that would indeed be a good idea. However, the question arises which  
examples to use. I would go for all TRSs where full termination has  
not already been proven.

Cheers,
René

PS: Attached a preliminary list:

AG01__4.12a.trs
AG01__4.13.trs
AG01__4.14.trs
AG01__4.15.trs
AG01__4.16.trs
AG01__4.17.trs
AG01__4.18.trs
AG01__4.19.trs
AG01__4.2.trs
AG01__4.3.trs
AG01__4.4.trs
AG01__4.5.trs
AG01__4.7.trs
AProVE__JFP_Ex31.trs
cariboo__ex1.trs
cariboo__ex2.trs
cariboo__ex3.trs
cariboo__ex4.trs
cariboo__ex5.trs
cariboo__ex6.trs
Cime__append-wrong.trs
Cime__maude2.trs
currying__AG01__4.10.trs
currying__AG01__4.13.trs
currying__AG01__4.15.trs
currying__AG01__4.17.trs
currying__AG01__4.19.trs
currying__AG01__4.2.trs
currying__AG01__4.3.trs
currying__AG01__4.5.trs
currying__AG01__4.7.trs
currying__AG01__4.8.trs
currying__D33__33.trs
currying__Ste92__minsort.trs
D33__33.trs
Endrullis__linear2.trs
Endrullis__pair2hard.trs
Endrullis__pair2simple2.trs
Endrullis__pair3swap.trs
Endrullis__quadruple2.trs
higher-order__AotoYam__001.trs
higher-order__AotoYam__003.trs
higher-order__AotoYam__Ex5TermProof.trs
higher-order__AProVE_HO__nonTermF.trs
higher-order__AProVE_HO__termMonTypes.trs
higher-order__AProVE_HO__TypeEx3.trs
higher-order__AProVE_HO__TypeEx5.trs
higher-order__Bird__Ex2_8_1ConstSubstFix.trs
higher-order__Bird__Hamming.trs
higher-order__Lifantsev__Ex10Functional.trs
higher-order__Lifantsev__Ex2PrimRec.trs
higher-order__Lifantsev__Ex5Sorting.trs
higher-order__Lifantsev__Ex6Folding.trs
higher-order__Lifantsev__Ex7OrdinalRec.trs
higher-order__Lifantsev__Ex9Maps.trs
higher-order__ToyamaRTA04__Ex5Folding.trs
higher-order__ToyamaRTA04__Ex6Recursor.trs
higher-order__ToyamaRTA04__Ex7Sorting.trs
HM__n001.trs
HM__n002.trs
HM__n003.trs
HM__n004.trs
HM__n005.trs
HM__n006.trs
HM__n007.trs
HofWald__6.trs
HofWald__7.trs
nontermin__CSR__Ex14_AEGL02.trs
nontermin__CSR__Ex15_Luc98.trs
nontermin__CSR__Ex1_2_AEL03.trs
nontermin__CSR__Ex1_2_Luc02c.trs
nontermin__CSR__Ex1_GL02a.trs
nontermin__CSR__Ex1_GM03.trs
nontermin__CSR__Ex1_GM99.trs
nontermin__CSR__Ex1_Luc02b.trs
nontermin__CSR__Ex1_Zan97.trs
nontermin__CSR__Ex24_GM04.trs
nontermin__CSR__Ex26_Luc03b.trs
nontermin__CSR__Ex2_Luc03b.trs
nontermin__CSR__Ex3_12_Luc96a.trs
nontermin__CSR__Ex3_2_Luc97.trs
nontermin__CSR__Ex3_3_25_Bor03.trs
nontermin__CSR__Ex4_4_Luc96b.trs
nontermin__CSR__Ex4_7_15_Bor03.trs
nontermin__CSR__Ex4_7_37_Bor03.trs
nontermin__CSR__Ex4_7_56_Bor03.trs
nontermin__CSR__Ex4_7_77_Bor03.trs
nontermin__CSR__Ex4_Zan97.trs
nontermin__CSR__Ex5_7_Luc97.trs
nontermin__CSR__Ex5_Zan97.trs
nontermin__CSR__Ex6_15_AEL02.trs
nontermin__CSR__Ex6_9_Luc02c.trs
nontermin__CSR__Ex6_GM04.trs
nontermin__CSR__Ex6_Luc98.trs
nontermin__CSR__Ex7_BLR02.trs
nontermin__CSR__Ex8_BLR02.trs
nontermin__CSR__Ex9_BLR02.trs
nontermin__CSR__ExAppendixB_AEL03.trs
nontermin__CSR__ExConc_Zan97.trs
nontermin__CSR__ExIntrod_GM01.trs
nontermin__CSR__ExIntrod_GM04.trs
nontermin__CSR__ExIntrod_GM99.trs
nontermin__CSR__ExIntrod_Zan97.trs
nontermin__TRCSR__ExSec11_1_Luc02a.trs
Rubio-inn__bn111.trs
Rubio-inn__gkg.trs
Rubio-inn__muladd.trs
Rubio-inn__test10.trs
Rubio-inn__test75.trs
Rubio-inn__test76.trs
Rubio-inn__test77.trs
Rubio-inn__test9.trs
Rubio-inn__toyama.trs
SchneiderKamp__inn__cade04.trs
SchneiderKamp__inn__cade05.trs
SchneiderKamp__inn__cade12.trs
SchneiderKamp__inn__cade13.trs
SchneiderKamp__inn__thiemann26i.trs
SchneiderKamp__inn__thiemann28i.trs
SchneiderKamp__inn__wiehe13.trs
SchneiderKamp__inn__wiehe14.trs
SchneiderKamp__trs__cade04t.trs
SchneiderKamp__trs__cade12t.trs
SchneiderKamp__trs__cade17.trs
SchneiderKamp__trs__thiemann21.trs
SchneiderKamp__trs__thiemann30.trs
SchneiderKamp__trs__thiemann40.trs
SchneiderKamp__trs__wiehe01.trs
SchneiderKamp__trs__wiehe02.trs
SchneiderKamp__trs__wiehe03.trs
SchneiderKamp__trs__wiehe05.trs
SchneiderKamp__trs__wiehe06.trs
SchneiderKamp__trs__wiehe07.trs
SchneiderKamp__trs__wiehe08.trs
SchneiderKamp__trs__wiehe09.trs
SchneiderKamp__trs__wiehe11.trs
SchneiderKamp__trs__wiehe12.trs
secret05__cime1.trs
secret05__cime3.trs
secret05__cime4.trs
secret05__teparla3.trs
secret05__tpa3.trs
secret05__tpa4.trs
secret05__tpa5.trs
secret05__ttt1.trs
secret05__ttt2.trs
secret06__cime1.trs
secret06__jambox2.trs
secret06__jambox3.trs
secret06__jambox5.trs
secret06__matchbox-gen-25.trs
secret06__matchbox-gen-28.trs
secret06__tpa01.trs
secret06__tpa02.trs
secret06__tpa03.trs
secret06__tpa04.trs
secret06__tpa05.trs
secret06__tpa06.trs
secret06__tpa07.trs
secret06__tpa08.trs
secret06__tpa09.trs
secret07__aprove03.trs
SK90__2.05.trs
SK90__4.06.trs
SK90__4.34.trs
SK90__4.40.trs
SK90__4.49.trs
SK90__4.54.trs
Ste92__minsort.trs
Thiemann__div_notTermin.trs
Thiemann__innermost1.trs
Thiemann__innermost2.trs
Thiemann__innermost3.trs
Thiemann__innermost4.trs
Thiemann__innermost5.trs
Thiemann__nonterm.trs
TRCSR__Ex14_AEGL02_C.trs
TRCSR__Ex14_AEGL02_FR.trs
TRCSR__Ex14_AEGL02_L.trs
TRCSR__Ex14_AEGL02_Z.trs
TRCSR__Ex14_Luc06_C.trs
TRCSR__Ex14_Luc06_FR.trs
TRCSR__Ex14_Luc06_GM.trs
TRCSR__Ex14_Luc06_iGM.trs
TRCSR__Ex14_Luc06_L.trs
TRCSR__Ex15_Luc06_L.trs
TRCSR__Ex15_Luc98_FR.trs
TRCSR__Ex16_Luc06_L.trs
TRCSR__Ex1_2_AEL03_C.trs
TRCSR__Ex1_2_AEL03_GM.trs
TRCSR__Ex1_2_AEL03_iGM.trs
TRCSR__Ex1_GL02a_FR.trs
TRCSR__Ex1_GL02a_L.trs
TRCSR__Ex1_GL02a_Z.trs
TRCSR__Ex1_GM03_C.trs
TRCSR__Ex1_GM03_FR.trs
TRCSR__Ex1_GM03_GM.trs
TRCSR__Ex1_GM03_iGM.trs
TRCSR__Ex1_GM03_Z.trs
TRCSR__Ex1_GM99_FR.trs
TRCSR__Ex1_GM99_GM.trs
TRCSR__Ex1_GM99_iGM.trs
TRCSR__Ex1_GM99_L.trs
TRCSR__Ex1_Luc02b_C.trs
TRCSR__Ex1_Luc02b_GM.trs
TRCSR__Ex1_Luc02b_iGM.trs
TRCSR__Ex1_Luc04b_FR.trs
TRCSR__Ex1_Luc04b_Z.trs
TRCSR__Ex1_Zan97_FR.trs
TRCSR__Ex1_Zan97_L.trs
TRCSR__Ex24_GM04_C.trs
TRCSR__Ex24_GM04_FR.trs
TRCSR__Ex24_GM04_GM.trs
TRCSR__Ex24_GM04_iGM.trs
TRCSR__Ex24_GM04_L.trs
TRCSR__Ex24_GM04_Z.trs
TRCSR__Ex24_Luc06_FR.trs
TRCSR__Ex24_Luc06_GM.trs
TRCSR__Ex24_Luc06_iGM.trs
TRCSR__Ex24_Luc06_L.trs
TRCSR__Ex26_Luc03b_FR.trs
TRCSR__Ex26_Luc03b_Z.trs
TRCSR__Ex2_Luc02a_C.trs
TRCSR__Ex2_Luc02a_GM.trs
TRCSR__Ex2_Luc02a_iGM.trs
TRCSR__Ex3_12_Luc96a_C.trs
TRCSR__Ex3_12_Luc96a_GM.trs
TRCSR__Ex3_12_Luc96a_iGM.trs
TRCSR__Ex3_2_Luc97_C.trs
TRCSR__Ex3_2_Luc97_FR.trs
TRCSR__Ex3_2_Luc97_GM.trs
TRCSR__Ex3_2_Luc97_iGM.trs
TRCSR__Ex3_2_Luc97_Z.trs
TRCSR__Ex3_3_25_Bor03_FR.trs
TRCSR__Ex3_3_25_Bor03_Z.trs
TRCSR__Ex49_GM04_C.trs
TRCSR__Ex49_GM04_FR.trs
TRCSR__Ex4_4_Luc96b_FR.trs
TRCSR__Ex4_4_Luc96b_Z.trs
TRCSR__Ex4_7_37_Bor03_C.trs
TRCSR__Ex4_7_37_Bor03_GM.trs
TRCSR__Ex4_7_37_Bor03_iGM.trs
TRCSR__Ex4_7_56_Bor03_C.trs
TRCSR__Ex4_7_56_Bor03_GM.trs
TRCSR__Ex4_7_56_Bor03_iGM.trs
TRCSR__Ex4_DLMMU04_C.trs
TRCSR__Ex4_DLMMU04_FR.trs
TRCSR__Ex4_DLMMU04_GM.trs
TRCSR__Ex4_DLMMU04_iGM.trs
TRCSR__Ex4_DLMMU04_Z.trs
TRCSR__Ex4_Zan97_C.trs
TRCSR__Ex4_Zan97_GM.trs
TRCSR__Ex4_Zan97_iGM.trs
TRCSR__Ex5_7_Luc97_C.trs
TRCSR__Ex5_7_Luc97_FR.trs
TRCSR__Ex5_7_Luc97_GM.trs
TRCSR__Ex5_7_Luc97_iGM.trs
TRCSR__Ex5_7_Luc97_Z.trs
TRCSR__Ex5_DLMMU04_C.trs
TRCSR__Ex5_DLMMU04_FR.trs
TRCSR__Ex5_DLMMU04_Z.trs
TRCSR__Ex6_15_AEL02_C.trs
TRCSR__Ex6_15_AEL02_FR.trs
TRCSR__Ex6_15_AEL02_GM.trs
TRCSR__Ex6_15_AEL02_iGM.trs
TRCSR__Ex6_15_AEL02_Z.trs
TRCSR__Ex6_GM04_FR.trs
TRCSR__Ex7_BLR02_C.trs
TRCSR__Ex7_BLR02_GM.trs
TRCSR__Ex7_BLR02_iGM.trs
TRCSR__Ex8_BLR02_C.trs
TRCSR__Ex8_BLR02_GM.trs
TRCSR__Ex8_BLR02_iGM.trs
TRCSR__Ex9_BLR02_C.trs
TRCSR__Ex9_BLR02_FR.trs
TRCSR__Ex9_Luc04_C.trs
TRCSR__Ex9_Luc04_FR.trs
TRCSR__Ex9_Luc04_GM.trs
TRCSR__Ex9_Luc04_iGM.trs
TRCSR__Ex9_Luc04_L.trs
TRCSR__Ex9_Luc06_FR.trs
TRCSR__ExAppendixB_AEL03_C.trs
TRCSR__ExAppendixB_AEL03_GM.trs
TRCSR__ExAppendixB_AEL03_iGM.trs
TRCSR__ExConc_Zan97_Z.trs
TRCSR__ExIntrod_GM01_FR.trs
TRCSR__ExIntrod_GM01_Z.trs
TRCSR__ExIntrod_GM04_FR.trs
TRCSR__ExIntrod_GM04_Z.trs
TRCSR__ExIntrod_GM99_C.trs
TRCSR__ExIntrod_GM99_FR.trs
TRCSR__ExIntrod_GM99_GM.trs
TRCSR__ExIntrod_GM99_iGM.trs
TRCSR__ExIntrod_GM99_Z.trs
TRCSR__ExIntrod_Zan97_C.trs
TRCSR__ExIntrod_Zan97_FR.trs
TRCSR__ExIntrod_Zan97_GM.trs
TRCSR__ExIntrod_Zan97_iGM.trs
TRCSR__ExIntrod_Zan97_Z.trs
TRCSR__ExSec11_1_Luc02a_C.trs
TRCSR__ExSec11_1_Luc02a_GM.trs
TRCSR__ExSec11_1_Luc02a_iGM.trs
TRCSR__ExSec4_2_DLMMU04_C.trs
TRCSR__ExSec4_2_DLMMU04_GM.trs
TRCSR__ExSec4_2_DLMMU04_iGM.trs
TRCSR__inn__LengthOfFiniteLists_complete_C.trs
TRCSR__inn__LengthOfFiniteLists_complete_iGM.trs
TRCSR__inn__LengthOfFiniteLists_complete_noand_C.trs
TRCSR__inn__LengthOfFiniteLists_complete_noand_iGM.trs
TRCSR__inn__LengthOfFiniteLists_nokinds_C.trs
TRCSR__inn__LengthOfFiniteLists_nokinds_iGM.trs
TRCSR__inn__LengthOfFiniteLists_nokinds_noand_C.trs
TRCSR__inn__LengthOfFiniteLists_nosorts_C.trs
TRCSR__inn__LengthOfFiniteLists_nosorts_GM.trs
TRCSR__inn__LengthOfFiniteLists_nosorts_iGM.trs
TRCSR__inn__LengthOfFiniteLists_nosorts_noand_C.trs
TRCSR__inn__LengthOfFiniteLists_nosorts_noand_GM.trs
TRCSR__inn__LengthOfFiniteLists_nosorts_noand_iGM.trs
TRCSR__inn__LISTUTILITIES_complete_C.trs
TRCSR__inn__LISTUTILITIES_complete_GM.trs
TRCSR__inn__LISTUTILITIES_complete_iGM.trs
TRCSR__inn__LISTUTILITIES_complete_noand_C.trs
TRCSR__inn__LISTUTILITIES_complete_noand_GM.trs
TRCSR__inn__LISTUTILITIES_complete_noand_iGM.trs
TRCSR__inn__LISTUTILITIES_nokinds_C.trs
TRCSR__inn__LISTUTILITIES_nokinds_GM.trs
TRCSR__inn__LISTUTILITIES_nokinds_iGM.trs
TRCSR__inn__LISTUTILITIES_nokinds_noand_C.trs
TRCSR__inn__LISTUTILITIES_nokinds_noand_GM.trs
TRCSR__inn__LISTUTILITIES_nokinds_noand_iGM.trs
TRCSR__inn__LISTUTILITIES_nosorts_C.trs
TRCSR__inn__LISTUTILITIES_nosorts_GM.trs
TRCSR__inn__LISTUTILITIES_nosorts_iGM.trs
TRCSR__inn__LISTUTILITIES_nosorts_noand_C.trs
TRCSR__inn__LISTUTILITIES_nosorts_noand_GM.trs
TRCSR__inn__LISTUTILITIES_nosorts_noand_iGM.trs
TRCSR__inn__MYNAT_complete_C.trs
TRCSR__inn__MYNAT_complete_GM.trs
TRCSR__inn__MYNAT_complete_iGM.trs
TRCSR__inn__MYNAT_complete_noand_C.trs
TRCSR__inn__MYNAT_complete_noand_GM.trs
TRCSR__inn__MYNAT_complete_noand_iGM.trs
TRCSR__inn__MYNAT_nokinds_C.trs
TRCSR__inn__MYNAT_nokinds_GM.trs
TRCSR__inn__MYNAT_nokinds_iGM.trs
TRCSR__inn__MYNAT_nokinds_noand_C.trs
TRCSR__inn__MYNAT_nokinds_noand_GM.trs
TRCSR__inn__MYNAT_nokinds_noand_iGM.trs
TRCSR__inn__MYNAT_nosorts_C.trs
TRCSR__inn__MYNAT_nosorts_iGM.trs
TRCSR__inn__MYNAT_nosorts_noand_C.trs
TRCSR__inn__MYNAT_nosorts_noand_iGM.trs
TRCSR__inn__OvConsOS_complete_C.trs
TRCSR__inn__OvConsOS_complete_GM.trs
TRCSR__inn__OvConsOS_complete_iGM.trs
TRCSR__inn__OvConsOS_complete_noand_C.trs
TRCSR__inn__OvConsOS_complete_noand_GM.trs
TRCSR__inn__OvConsOS_complete_noand_iGM.trs
TRCSR__inn__OvConsOS_nokinds_C.trs
TRCSR__inn__OvConsOS_nokinds_GM.trs
TRCSR__inn__OvConsOS_nokinds_iGM.trs
TRCSR__inn__OvConsOS_nokinds_noand_C.trs
TRCSR__inn__OvConsOS_nokinds_noand_iGM.trs
TRCSR__inn__OvConsOS_nosorts_C.trs
TRCSR__inn__OvConsOS_nosorts_GM.trs
TRCSR__inn__OvConsOS_nosorts_iGM.trs
TRCSR__inn__OvConsOS_nosorts_noand_C.trs
TRCSR__inn__OvConsOS_nosorts_noand_GM.trs
TRCSR__inn__OvConsOS_nosorts_noand_iGM.trs
TRCSR__inn__PALINDROME_complete_C.trs
TRCSR__inn__PALINDROME_complete_noand_C.trs
TRCSR__inn__PALINDROME_complete_noand_iGM.trs
TRCSR__inn__PEANO_complete_C.trs
TRCSR__inn__PEANO_complete_noand_C.trs
TRCSR__inn__PEANO_nokinds_C.trs
TRCSR__inn__PEANO_nokinds_noand_C.trs
TRCSR__LengthOfFiniteLists_complete-noand_FR.trs
TRCSR__LengthOfFiniteLists_complete-noand_Z.trs
TRCSR__LengthOfFiniteLists_complete_FR.trs
TRCSR__LengthOfFiniteLists_complete_Z.trs
TRCSR__LengthOfFiniteLists_nokinds-noand_FR.trs
TRCSR__LengthOfFiniteLists_nokinds-noand_Z.trs
TRCSR__LengthOfFiniteLists_nokinds_FR.trs
TRCSR__LengthOfFiniteLists_nokinds_Z.trs
TRCSR__LengthOfFiniteLists_nosorts-noand_FR.trs
TRCSR__LengthOfFiniteLists_nosorts_FR.trs
TRCSR__LISTUTILITIES_complete-noand_FR.trs
TRCSR__LISTUTILITIES_complete-noand_Z.trs
TRCSR__LISTUTILITIES_complete_FR.trs
TRCSR__LISTUTILITIES_complete_Z.trs
TRCSR__LISTUTILITIES_nokinds-noand_FR.trs
TRCSR__LISTUTILITIES_nokinds-noand_Z.trs
TRCSR__LISTUTILITIES_nokinds_FR.trs
TRCSR__LISTUTILITIES_nokinds_Z.trs
TRCSR__MYNAT_complete-noand_FR.trs
TRCSR__MYNAT_complete-noand_Z.trs
TRCSR__MYNAT_complete_FR.trs
TRCSR__MYNAT_complete_Z.trs
TRCSR__MYNAT_nokinds_FR.trs
TRCSR__MYNAT_nokinds_Z.trs
TRCSR__OvConsOS_complete-noand_FR.trs
TRCSR__OvConsOS_complete-noand_Z.trs
TRCSR__OvConsOS_complete_FR.trs
TRCSR__OvConsOS_complete_Z.trs
TRCSR__OvConsOS_nokinds-noand_FR.trs
TRCSR__OvConsOS_nokinds-noand_Z.trs
TRCSR__OvConsOS_nokinds_FR.trs
TRCSR__OvConsOS_nokinds_Z.trs
TRCSR__OvConsOS_nosorts-noand_FR.trs
TRCSR__OvConsOS_nosorts-noand_Z.trs
TRCSR__OvConsOS_nosorts_FR.trs
TRCSR__OvConsOS_nosorts_Z.trs
TRCSR__PALINDROME_complete-noand_L.trs
TRCSR__PALINDROME_nokinds-noand_L.trs
TRCSR__PEANO_complete_FR.trs
various__04.trs
various__05.trs
various__08.trs
Waldmann__jwno1.trs
Waldmann__jwno2.trs
Waldmann__jwno3.trs
Waldmann__jwno4.trs
Waldmann__jwno5.trs
Waldmann__jwno6.trs
Waldmann__jwno7.trs
Waldmann__jwno8.trs
Waldmann__jwno9.trs
Zantema06__hydra.trs
Zantema06__while2.trs
Zantema__z09.trs
Zantema__z10.trs
Zantema__z17.trs
Zantema__z20.trs
-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck