توسعه روش SL با ترتيب KBO براي اثبات خودكار پايان‌پذيري سيستم بازنويسي ترم

سيستم بازنويسي ترم (TRS)مدلي انتزاعي از زبان هاي تابعي ارايه مي دهد.اثبات پايان پذيرييكTRSبراي تاييد درستي عملكرد زبان‌هاي تابعيضروري است.روش برچسب گذاري معنايي(SL)روشي كامل براي اثبات پايان پذيري به شمار مي رود. بخش معنايياين روش توسط يك شبه‌ـ مدلاز تفسير تابع نشانه ها ايجاد مي شود. بيشتر توان روش SLبه استفاده از مدل هاي نامتناهي مربوط مي شود كهارايهآن‌ها در ابزارهاي آزمون خودكار پايان پذيري دشوار است. در اين مقاله،روش SL با دامنه تفسيراعداد طبيعي به شكلي با ترتيب كُنت‌ـ بنديكس (KBO) تركيب شده تا بتوان اثبات پايان پذيري با مدل هاي نامتناهي را به طور خودكار انجام داد. ابتدا تعميمي از KBO به نام ترتيب كُنت‌ـ بنديكس برچسب گذاري(?KBO)ارايه، سپس توانايي آن را در اثبات پايان پذيري TRS نشان داده ايم. الگوريتم جستجوي خودكار يك ?KBO براي يك TRSمعرفيشده و عملكرد آن روي كتابخانهTPDB 3.1 با موفقيت، مورد آزمون قرار گرفته است