KBO Orientability

KBO Orientability

Harald Zankl

Nao Hirokawa

Aart Middeldorp

† Japan Advanced Institute of Science and Technology

‡ University of Innsbruck

Reference

JAR 2009 Harald Zankl, Nao Hirokawa, and Aart Middeldorp KBO Orientability

Journal of Automated Reasoning 43(2), pp. 173-201, 2009

Term Rewriting

Definition

pair of terms l→ris rewrite rule ifl6∈ V ∧ Var(r)⊆ Var(l) term rewrite system(TRS) is set of rewrite rules

(rewrite relation)s→_R tif∃l→r∈ R,contextC,substitutionσ.

s=C[lσ] ∧ t=C[rσ]

Example

TRSR

x+0→x x+s(y)→s(x+y)

x×0→0 x×s(y)→x×y+x

rewriting

s(0)×s(0)→Rs(0)×0+s(0)

→R0+s(0)

→Rs(0+0)

→Rs(0) terminated

Term Rewriting

Definition

pair of terms l→ris rewrite rule ifl6∈ V ∧ Var(r)⊆ Var(l) term rewrite system(TRS) is set of rewrite rules

(rewrite relation)s→_R tif∃l→r∈ R,contextC,substitutionσ.

s=C[lσ] ∧ t=C[rσ]

Example

TRSR

x+0→x x+s(y)→s(x+y)

x×0→0 x×s(y)→x×y+x

rewriting

s(0)×s(0)→Rs(0)×0+s(0)

→R0+s(0)

→Rs(0+0)

→Rs(0) terminated

Term Rewriting

Definition

pair of terms l→ris rewrite rule ifl6∈ V ∧ Var(r)⊆ Var(l) term rewrite system(TRS) is set of rewrite rules

(rewrite relation)s→_R tif∃l→r∈ R,contextC,substitutionσ.

s=C[lσ] ∧ t=C[rσ]

Example

TRSR

x+0→x x+s(y)→s(x+y)

x×0→0 x×s(y)→x×y+x

rewriting

s(0)×s(0)→Rs(0)×0+s(0)

→R0+s(0)

→Rs(0+0)

Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1→_Rt2→_R· · ·

QUESTION

how to prove termination?

+ Knuth-Bendix order (KBO)

introduced by Knuth and Bendix, 1970 best studied termination methods

great success intheorem provers (Waldmeister, Vampire, ...)

Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1→_Rt2→_R· · ·

QUESTION

how to prove termination?

+ Knuth-Bendix order (KBO)

introduced by Knuth and Bendix, 1970 best studied termination methods

great success intheorem provers (Waldmeister, Vampire, ...)

Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1→_Rt2→_R· · ·

QUESTION

how to prove termination?

+ Knuth-Bendix order (KBO)

introduced by Knuth and Bendix, 1970 best studied termination methods

great success intheorem provers (Waldmeister, Vampire, ...)

Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1→_Rt2→_R· · ·

QUESTION

how to prove termination?

+ Knuth-Bendix order (KBO)

introduced by Knuth and Bendix, 1970

best studied termination methods

great success intheorem provers (Waldmeister, Vampire, ...)

Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1→_Rt2→_R· · ·

QUESTION

how to prove termination?

+ Knuth-Bendix order (KBO)

introduced by Knuth and Bendix, 1970 best studied termination methods

great success intheorem provers (Waldmeister, Vampire, ...)

Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1→_Rt2→_R· · ·

QUESTION

how to prove termination?

+ Knuth-Bendix order (KBO)

introduced by Knuth and Bendix, 1970 best studied termination methods

great success intheorem provers (Waldmeister, Vampire, ...)

Knuth-Bendix Orders

Definition

precedence>is proper order on function symbolsF

weight function (w, w0)is pair inR>0F×R>0

weight of termtis

w(t) =

(w₀ ift∈ V

w(f) +w(t1) +· · ·+w(tn) ift=f(t1, . . . , tn)

weight function (w, w0)isadmissiblefor precedence >if w(f)>0 or f >g

for all unary functionsf and all functionsg

Knuth-Bendix Orders

Definition

precedence>is proper order on function symbolsF weight function (w, w0)is pair inR>0F×R>0

weight of termtis

w(t) =

(w₀ ift∈ V

w(f) +w(t1) +· · ·+w(tn) ift=f(t1, . . . , tn)

weight function (w, w0)isadmissiblefor precedence >if w(f)>0 or f >g

for all unary functionsf and all functionsg

Knuth-Bendix Orders

Definition

precedence>is proper order on function symbolsF weight function (w, w0)is pair inR>0F×R>0

weight of termtis

w(t) =

(w₀ ift∈ V

w(f) +w(t1) +· · ·+w(tn) ift=f(t1, . . . , tn)

weight function (w, w0)isadmissiblefor precedence >if w(f)>0 or f >g

for all unary functionsf and all functionsg

Knuth-Bendix Orders

Definition

precedence>is proper order on function symbolsF weight function (w, w0)is pair inR>0F×R>0

weight of termtis

w(t) =

(w₀ ift∈ V

w(f) +w(t1) +· · ·+w(tn) ift=f(t1, . . . , tn)

weight function (w, w0)isadmissiblefor precedence>if w(f)>0 or f >g

for all unary functionsf and all functionsg

Definition

Knuth-Bendix order>kbo on termsT(F,V):

s >kbot if|s|x>|t|x for allx∈ V and either

w(s)> w(t), or

w(s) =w(t)and

s=fⁿ(t)andt∈ Vfor some unaryf andn>1; or

s=f(s1, . . . , si−1, si, . . . , sn),t=f(s1, . . . , si−1, ti, . . . , tn), and si>kboti; or

s=f(s1, . . . , sn),t=g(t1, . . . , tm), andf > g

Definition

Knuth-Bendix order>kbo on termsT(F,V):

s >kbot if|s|x>|t|x for allx∈ V and either w(s)> w(t), or

w(s) =w(t)and

s=fⁿ(t)andt∈ Vfor some unaryf andn>1; or

s=f(s1, . . . , si−1, si, . . . , sn),t=f(s1, . . . , si−1, ti, . . . , tn), and si>kboti; or

s=f(s1, . . . , sn),t=g(t1, . . . , tm), andf > g

Definition

Knuth-Bendix order>kbo on termsT(F,V):

s >kbot if|s|x>|t|x for allx∈ V and either w(s)> w(t), or

w(s) =w(t)and

s=fⁿ(t)andt∈ Vfor some unaryf andn>1; or

s=f(s1, . . . , si−1, si, . . . , sn),t=f(s1, . . . , si−1, ti, . . . , tn), and si>kboti; or

s=f(s1, . . . , sn),t=g(t1, . . . , tm), andf > g

Definition

Knuth-Bendix order>kbo on termsT(F,V):

s >kbot if|s|x>|t|x for allx∈ V and either w(s)> w(t), or

w(s) =w(t)and

s=fⁿ(t)andt∈ Vfor some unaryf andn>1; or

s=f(s1, . . . , si−1, si, . . . , sn),t=f(s1, . . . , si−1, ti, . . . , tn), and si>kboti; or

s=f(s1, . . . , sn),t=g(t1, . . . , tm), andf > g

Definition

Knuth-Bendix order>kbo on termsT(F,V):

s >kbot if|s|x>|t|x for allx∈ V and either w(s)> w(t), or

w(s) =w(t)and

s=fⁿ(t)andt∈ Vfor some unaryf andn>1; or

s=f(s1, . . . , si−1, si, . . . , sn),t=f(s1, . . . , si−1, ti, . . . , tn), and si>kboti; or

s=f(s1, . . . , sn),t=g(t1, . . . , tm), andf > g

Definition

Knuth-Bendix order>kbo on termsT(F,V):

s >kbot if|s|x>|t|x for allx∈ V and either w(s)> w(t), or

w(s) =w(t)and

s=fⁿ(t)andt∈ Vfor some unaryf andn>1; or

s=f(s1, . . . , si−1, si, . . . , sn),t=f(s1, . . . , si−1, ti, . . . , tn), and si>kboti; or

s=f(s1, . . . , sn),t=g(t1, . . . , tm), andf > g

Definition

letX ⊆R>0. TRSRisKBOX terminatingif

∃ precedence>

∃ admissible weight function(w, w0)∈X^F×X such thatl >_kborfor alll→r∈ R

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBO_N terminating

Definition

letX ⊆R>0. TRSRisKBOX terminatingif

∃ precedence>

∃ admissible weight function(w, w0)∈X^F×X such thatl >_kborfor alll→r∈ R

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBO_N terminating

Quiz

Example I

a(a(x))→b(b(b(x))) b(b(b(b(b(x)))))→a(a(a(x)))

is KBO_Nterminating ? — yes

Proof

take precedencea>band weight function w(a) =

?3

w(b) =

?2

w₀= 1

Proof

another solution: take precedence>=∅and weight function w(a) =

?13

w(b) =

?8

w0= 1

Example I

a(a(x))→b(b(b(x))) b(b(b(b(b(x)))))→a(a(a(x)))

is KBO_Nterminating ?

—yes

Proof

take precedencea>band weight function w(a) =

?3

w(b) =

?2

w₀= 1

Proof

another solution: take precedence>=∅and weight function w(a) =

?13

w(b) =

?8

w0= 1

Example I

a(a(x))→b(b(b(x))) b(b(b(b(b(x)))))→a(a(a(x)))

is KBO_Nterminating ? — yes

Proof

take precedencea>band weight function w(a) = ?

3

w(b) = ?

2

w₀= 1

Proof

another solution: take precedence>=∅and weight function

w(a) =

?13

w(b) =

?8

w0= 1

Example I

a(a(x))→b(b(b(x))) b(b(b(b(b(x)))))→a(a(a(x)))

is KBO_Nterminating ? — yes

Proof

take precedencea>band weight function w(a) =

?

3 w(b) =

?

2 w₀= 1

Proof

another solution: take precedence>=∅and weight function w(a) =

?13

w(b) =

?8

w0= 1

Example I

a(a(x))→b(b(b(x))) b(b(b(b(b(x)))))→a(a(a(x)))

is KBO_Nterminating ? — yes

Proof

take precedencea>band weight function w(a) =

?

3 w(b) =

?

2 w₀= 1

Proof

another solution: take precedence>=∅and weight function w(a) = ?

13

w(b) = ?

8

w0= 1

Example I

a(a(x))→b(b(b(x))) b(b(b(b(b(x)))))→a(a(a(x)))

is KBO_Nterminating ? — yes

Proof

take precedencea>band weight function w(a) =

?

3 w(b) =

?

2 w₀= 1

Proof

another solution: take precedence>=∅and weight function w(a) =

?

13 w(b) =

?

8 w0= 1

Example II

TRSR

x+0→x x+s(y)→s(x+y) x×0→0 x×s(y)→x×y+x is KBO_Nterminating ?

—no

Example II

TRSR

x+0→x x+s(y)→s(x+y) x×0→0 x×s(y)→x×y+x is KBO_Nterminating ? — no

History of KBO

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBO_N terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBO_R>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBO_R>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBO_Nterminating ⇐⇒ it is KBO_R>0 terminating

KBO_R>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

KBO{0,1,...,B} termination (B∈N) can reduce toSATandPBC

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBO_N terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBO_R>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBO_R>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBO_Nterminating ⇐⇒ it is KBO_R>0 terminating

KBO_R>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

KBO{0,1,...,B} termination (B∈N) can reduce toSATandPBC

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBO_N terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBO_R>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBO_R>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBO_Nterminating ⇐⇒ it is KBO_R>0 terminating

KBO_R>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

KBO{0,1,...,B} termination (B∈N) can reduce toSATandPBC

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBO_N terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBO_R>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBO_R>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBO_Nterminating ⇐⇒ it is KBO_R>0 terminating

KBO_R>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

KBO{0,1,...,B} termination (B∈N) can reduce toSATandPBC

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBO_N terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBO_R>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBO_R>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBO_Nterminating ⇐⇒ it is KBO_R>0 terminating

KBO_R>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

KBO{0,1,...,B} termination (B∈N) can reduce toSATandPBC

This Talk

MAIN RESULT

for every TRSRandN =P

l→r∈R(|l|+|r|) + 1

Ris KBO_Nterminating ⇐⇒ Ris KBO{0,1,...,B} terminating where,B=N^4N+1

OVERVIEW OF PROOF

Principal Solutions

MCD

Bound by Norm

This Talk

MAIN RESULT

for every TRSRandN =P

l→r∈R(|l|+|r|) + 1

Ris KBO_Nterminating ⇐⇒ Ris KBO{0,1,...,B} terminating where,B=N^4N+1

OVERVIEW OF PROOF

Principal Solutions

MCD

Bound by Norm

This Talk

MAIN RESULT

for every TRSRandN =P

l→r∈R(|l|+|r|) + 1

Ris KBO_Nterminating ⇐⇒ Ris KBO{0,1,...,B} terminating where,B=N^4N+1

OVERVIEW OF PROOF

Principal Solutions

MCD

Bound by Norm

This Talk

MAIN RESULT

for every TRSRandN =P

l→r∈R(|l|+|r|) + 1

Ris KBO_Nterminating ⇐⇒ Ris KBO{0,1,...,B} terminating where,B=N^4N+1

OVERVIEW OF PROOF

Principal Solutions

MCD

Bound by Norm

Principal Solutions

Example

given precedence, KBO_Nproblem reduces tolinear integral constraints

Example

a(a(x))→b(b(b(x))) b(b(b(b(b(x)))))→a(a(a(x)))

for precedence a>b, solve wrtw(a), w(b)∈N 2·w(a)−3·w(b)>0 −3·w(a) + 5·w(b)>0

for precedence >=∅solve wrtw(a), w(b)∈N 2·w(a)−3·w(b)>0 −3·w(a) + 5·w(b)>0

Example

given precedence, KBO_Nproblem reduces tolinear integral constraints

Example

a(a(x))→b(b(b(x))) b(b(b(b(b(x)))))→a(a(a(x)))

for precedence a>b, solve wrtw(a), w(b)∈N 2·w(a)−3·w(b)>0 −3·w(a) + 5·w(b)>0

for precedence >=∅solve wrtw(a), w(b)∈N 2·w(a)−3·w(b)>0 −3·w(a) + 5·w(b)>0

Example

given precedence, KBO_Nproblem reduces tolinear integral constraints

Example

a(a(x))→b(b(b(x))) b(b(b(b(b(x)))))→a(a(a(x)))

for precedence a>b, solve wrtw(a), w(b)∈N 2·w(a)−3·w(b)>0 −3·w(a) + 5·w(b)>0

for precedence >=∅solve wrtw(a), w(b)∈N 2·w(a)−3·w(b)>0 −3·w(a) + 5·w(b)>0

Principal Solutions

Gale, 1960; Dick, Kalmus and Martin, 1990; Korovin and Voronkov, 2003

setI of KBO inequalities are of form

{ ~a_i·~x_i R_i 0 }_i with R_i∈{>, >},~a_i∈Zⁿ,~x∈N

Definition

writeAI for(~ai)1,...,n

~

xissolutionofA_I ifA_I~x>0and~x∈Nⁿ

solution~xmaximizing{i|~ai·~x >0} wrt⊆is principal

Theorem

principal solution ofA always exists

∀principal solution~x: (I is solvable ⇐⇒ ~xsatisfiesI)

Principal Solutions

Gale, 1960; Dick, Kalmus and Martin, 1990; Korovin and Voronkov, 2003

setI of KBO inequalities are of form

{ ~a_i·~x_i R_i 0 }_i with R_i∈{>, >},~a_i∈Zⁿ,~x∈N

Definition

writeAI for(~ai)1,...,n

~

xissolutionofA_I ifA_I~x>0and~x∈Nⁿ

solution~xmaximizing{i|~ai·~x >0} wrt⊆is principal

Theorem

principal solution ofA always exists

∀principal solution~x: (I is solvable ⇐⇒ ~xsatisfiesI)

Principal Solutions

Gale, 1960; Dick, Kalmus and Martin, 1990; Korovin and Voronkov, 2003

setI of KBO inequalities are of form

{ ~a_i·~x_i R_i 0 }_i with R_i∈{>, >},~a_i∈Zⁿ,~x∈N

Definition

writeAI for(~ai)1,...,n

~

xissolutionofA_I ifA_I~x>0and~x∈Nⁿ

solution~xmaximizing{i|~ai·~x >0} wrt⊆is principal

Theorem

principal solution ofA always exists

∀principal solution~x: (I is solvable ⇐⇒ ~xsatisfiesI)

Principal Solutions

Gale, 1960; Dick, Kalmus and Martin, 1990; Korovin and Voronkov, 2003

setI of KBO inequalities are of form

{ ~a_i·~x_i R_i 0 }_i with R_i∈{>, >},~a_i∈Zⁿ,~x∈N

Definition

writeAI for(~ai)1,...,n

~

xissolutionofA_I ifA_I~x>0and~x∈Nⁿ

solution~xmaximizing{i|~ai·~x >0} wrt⊆isprincipal

Theorem

principal solution ofA always exists

∀principal solution~x: (I is solvable ⇐⇒ ~xsatisfiesI)

Principal Solutions

Gale, 1960; Dick, Kalmus and Martin, 1990; Korovin and Voronkov, 2003

setI of KBO inequalities are of form

{ ~a_i·~x_i R_i 0 }_i with R_i∈{>, >},~a_i∈Zⁿ,~x∈N

Definition

writeAI for(~ai)1,...,n

~

xissolutionofA_I ifA_I~x>0and~x∈Nⁿ

solution~xmaximizing{i|~ai·~x >0} wrt⊆isprincipal

Theorem

principal solution ofA always exists

∀principal solution~x: (I is solvable ⇐⇒ ~xsatisfiesI)

I=

2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

AI =

2 −3

−3 5

since

AI

3 2

= 0

1

AI

13 8

= 2

1

3 2

is not principal solution ofAI

13 8

is principal solutionofA_I and satisfiesI hence I issolvable

I=

2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

AI =

2 −3

−3 5

since

AI

3 2

= 0

1

AI

13 8

= 2

1

3 2

is not principal solution ofAI

13 8

is principal solutionofA_I and satisfiesI hence I issolvable

I=

2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

AI =

2 −3

−3 5

since

AI

3 2

= 0

1

AI

13 8

= 2

1

3 2

is not principal solution ofAI

13 8

is principal solutionofA_I and satisfiesI hence Iis solvable

Example

I=







2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

−4·w(a) + 3·w(b) > 0







AI =





2 −3

−3 5

−4 3





principal solution ofAI is 0

0

anddoes notsatisfy I henceI is not solvable

QUESTION

how to findprincipal solution? + MCD

Example

I=







2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

−4·w(a) + 3·w(b) > 0







AI =





2 −3

−3 5

−4 3





principal solution ofAI is 0

0

anddoes notsatisfyI

henceI is not solvable

QUESTION

how to findprincipal solution? + MCD

Example

I=







2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

−4·w(a) + 3·w(b) > 0







AI =





2 −3

−3 5

−4 3





principal solution ofAI is 0

0

anddoes notsatisfyI henceI is not solvable

QUESTION

how to findprincipal solution? + MCD

Example

I=







2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

−4·w(a) + 3·w(b) > 0







AI =





2 −3

−3 5

−4 3





principal solution ofAI is 0

0

anddoes notsatisfyI henceI is not solvable

QUESTION

how to findprincipal solution?

+ MCD

Example

I=







2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

−4·w(a) + 3·w(b) > 0







AI =





2 −3

−3 5

−4 3





principal solution ofAI is 0

0

anddoes notsatisfyI henceI is not solvable

QUESTION

how to findprincipal solution? + MCD

MCD: Method of Complete Description

MCD

Dick, Kalmus and Martin, 1990 (a1, . . . , an)^κ= (~ei|ai>0) ++(aj~ei−ai~ej|ai<0, aj >0)

form×nmatrixA and06i6m S_i^A=

(En ifi= 0 S_i−1^A (~a_iS_i−1^A )^κ otherwise

sum of all column vectors of S_m^A is denoted by~s^A

Theorem

~s^Ais principal solutionofA

MCD

Dick, Kalmus and Martin, 1990 (a1, . . . , an)^κ= (~ei|ai>0) ++(aj~ei−ai~ej|ai<0, aj >0)

form×nmatrixA and06i6m S_i^A=

(En ifi= 0 S_i−1^A (~a_iS_i−1^A )^κ otherwise

sum of all column vectors of S_m^A is denoted by~s^A

Theorem

~s^Ais principal solutionofA

MCD

Dick, Kalmus and Martin, 1990 (a1, . . . , an)^κ= (~ei|ai>0) ++(aj~ei−ai~ej|ai<0, aj >0)

form×nmatrixA and06i6m S_i^A=

(En ifi= 0 S_i−1^A (~a_iS_i−1^A )^κ otherwise

sum of all column vectors ofS^A_mis denoted by~s^A

Theorem

~s^Ais principal solutionofA

MCD

Dick, Kalmus and Martin, 1990 (a1, . . . , an)^κ= (~ei|ai>0) ++(aj~ei−ai~ej|ai<0, aj >0)

form×nmatrixA and06i6m S_i^A=

(En ifi= 0 S_i−1^A (~a_iS_i−1^A )^κ otherwise

sum of all column vectors ofS^A_mis denoted by~s^A

Theorem

~s^Ais principal solutionofA

Example

I=

2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

AI =

2 −3

−3 5

performing MCD S₀^AI =

1 0 0 1

S₁^AI =S₀^AI((2 −3)S₀^AI)^κ= 1 3

0 2

S₂^AI =S₁^AI((−3 5)S₁^AI)^κ=

3 10 2 6

we obtain principal solution

~ s^AI =

3 2

+ 10

6

= 13

8

which satisfiesI. henceI is solvable

Example

I=

2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

AI =

2 −3

−3 5

performing MCD

S₀^AI = 1 0

0 1

S₁^AI =S₀^AI((2 −3)S₀^AI)^κ= 1 3

0 2

S₂^AI =S₁^AI((−3 5)S₁^AI)^κ=

3 10 2 6

we obtain principal solution

~ s^AI =

3 2

+ 10

6

= 13

8

which satisfiesI. henceI is solvable

Example

I=

2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

AI =

2 −3

−3 5

performing MCD S₀^AI =

1 0 0 1

S₁^AI =S₀^AI((2 −3)S₀^AI)^κ= 1 3

0 2

S₂^AI =S₁^AI((−3 5)S₁^AI)^κ=

3 10 2 6

we obtain principal solution

~ s^AI =

3 2

+ 10

6

= 13

8

which satisfiesI. henceI is solvable

Example

I=

2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

AI =

2 −3

−3 5

performing MCD S₀^AI =

1 0 0 1

S₁^AI =S₀^AI((2 −3)S₀^AI)^κ= 1 3

0 2

S₂^AI =S₁^AI((−3 5)S₁^AI)^κ=

3 10 2 6

we obtain principal solution

~s^AI = 3

2

+ 10

6

= 13

8

which satisfiesI. henceI is solvable

Example

I=

2·w(a)−3·w(b) > 0

−3·w(a) + 5·w(b) > 0

AI =

2 −3

−3 5

performing MCD S₀^AI =

1 0 0 1

S₁^AI =S₀^AI((2 −3)S₀^AI)^κ= 1 3

0 2

S₂^AI =S₁^AI((−3 5)S₁^AI)^κ=

3 10 2 6

we obtain principal solution

~s^AI = 3

2

+ 10

6

= 13

8

Bound by Norm

MCD

(a₁, . . . , a_n)^κ= (~e_i|a_i>0) ++(a_j~e_i−a_i~e_j|a_i<0, a_j >0)

form×nmatrixA and06i6m S_i^A=

(En ifi= 0 S_i−1^A (~a_iS_i−1^A )^κ otherwise

sum of all column vectors ofS^A_mis denoted by~s^A

GOAL

bound~s^A∈ {0,1, . . . , B}ⁿ

APPROACH

definenormk · kto calculatek~s^AIk withB=k~s^AIk

MCD

(a₁, . . . , a_n)^κ= (~e_i|a_i>0) ++(a_j~e_i−a_i~e_j|a_i<0, a_j >0)

form×nmatrixA and06i6m S_i^A=

(En ifi= 0 S_i−1^A (~a_iS_i−1^A )^κ otherwise

sum of all column vectors ofS^A_mis denoted by~s^A

GOAL

bound~s^A∈ {0,1, . . . , B}ⁿ

APPROACH

definenormk · kto calculatek~s^AIk withB=k~s^AIk

MCD

(a₁, . . . , a_n)^κ= (~e_i|a_i>0) ++(a_j~e_i−a_i~e_j|a_i<0, a_j >0)

form×nmatrixA and06i6m S_i^A=

(En ifi= 0 S_i−1^A (~a_iS_i−1^A )^κ otherwise

sum of all column vectors ofS^A_mis denoted by~s^A

GOAL

bound~s^A∈ {0,1, . . . , B}ⁿ

APPROACH

definenormk · kto calculatek~s^AIk withB=k~s^AIk

Norm

Definition

kAk= maxi,j|aij|form×nmatrixA= (aij)ij

Lemma

for everym×nmatrixAandn×pmatrixB ka^κk=kak

kABk6nkAkkBk

(a₁, . . . , a_n)^κ isn×kmatrix withk6n². S^A_i ism×kmatrix withk6n²ⁱ.

kS_i^Ak6(2mkAk)²ⁱ⁻¹ k~s^Ak6n^2m·(2mkAk)^2m−1

Norm

Definition

kAk= maxi,j|aij|form×nmatrixA= (aij)ij

Lemma

for everym×nmatrixAandn×pmatrixB ka^κk=kak

kABk6nkAkkBk

(a₁, . . . , a_n)^κ isn×kmatrix withk6n². S^A_i ism×kmatrix withk6n²ⁱ.

kS_i^Ak6(2mkAk)²ⁱ⁻¹ k~s^Ak6n^2m·(2mkAk)^2m−1

Norm

Definition

kAk= maxi,j|aij|form×nmatrixA= (aij)ij

Lemma

for everym×nmatrixAandn×pmatrixB ka^κk=kak

kABk6nkAkkBk

(a₁, . . . , a_n)^κ isn×kmatrix withk6n². S^A_i ism×kmatrix withk6n²ⁱ.

kS_i^Ak6(2mkAk)²ⁱ⁻¹ k~s^Ak6n^2m·(2mkAk)^2m−1

Norm

Definition

kAk= maxi,j|aij|form×nmatrixA= (aij)ij

Lemma

for everym×nmatrixAandn×pmatrixB ka^κk=kak

kABk6nkAkkBk

(a₁, . . . , a_n)^κ isn×kmatrix withk6n². S^A_i ism×kmatrix withk6n²ⁱ.

kS_i^Ak6(2mkAk)²ⁱ⁻¹ k~s^Ak6n^2m·(2mkAk)^2m−1

Norm

Definition

kAk= maxi,j|aij|form×nmatrixA= (aij)ij

Lemma

for everym×nmatrixAandn×pmatrixB ka^κk=kak

kABk6nkAkkBk

(a₁, . . . , a_n)^κ isn×kmatrix withk6n². S^A_i ism×kmatrix withk6n²ⁱ.

kS_i^Ak6(2mkAk)²ⁱ⁻¹ k~s^Ak6n^2m·(2mkAk)^2m−1

Lemma

letRbe TRS of sizeN

Ibe set of inequalities induced by KBO with fixed precedence AI be of sizem×n

m6N n6N kAIk6N therefore

k~s^AIk6N^4N+1:=B thus,

~s^AI ∈ {0,1, . . . , B}ⁿ

Main Result

Theorem

Ris KBO_Nterminating ⇐⇒ Ris KBO{0,1,...,B}terminating where,B=N^4N+1

Corollary

Zankl and Middeldorp’s SAT and PBC encodings are complete for thisB

Main Result

Theorem

Ris KBO_Nterminating ⇐⇒ Ris KBO{0,1,...,B}terminating where,B=N^4N+1

Corollary

Zankl and Middeldorp’s SAT and PBC encodings are complete for thisB

Summary

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N^4N+1 Ris KBO_R

>0 terminating

⇐⇒ Ris KBO_Nterminating Korovin and Voronkov

⇐⇒ Ris KBO{0,1,...,B} terminating this talk

theoretical interest of decidability issue is more or less closed

how about automation? +

Summary

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N^4N+1 Ris KBO_R

>0 terminating

⇐⇒ Ris KBO_Nterminating Korovin and Voronkov

⇐⇒ Ris KBO{0,1,...,B} terminating this talk

theoretical interest of decidability issue is more or less closed

how about automation? +

Summary

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N^4N+1 Ris KBO_R

>0 terminating

⇐⇒ Ris KBO_Nterminating Korovin and Voronkov

⇐⇒ Ris KBO{0,1,...,B} terminating this talk

theoretical interest of decidability issue is more or less closed

how about automation? +

Automation

Theorem Dick, Kalmus, and Martin, 1990

KBO_R>0 termination is decidable by MCD

Theorem Korovin and Voronkov, 2001, 2003

KBO_R>0 termination is decidable by Karmarkar/Khachiyanalgorithm

Theorem Zankl and Middeldorp, 2007

KBO{0,1,...,B} termination (B∈N) is decidable viaSAT/PBCencodings

Theorem

KBO_R

>0 termination is decidable viaSMT(linear arithmetic) encoding

Theorem Dick, Kalmus, and Martin, 1990

KBO_R>0 termination is decidable by MCD

Theorem Korovin and Voronkov, 2001, 2003

KBO_R>0 termination is decidable by Karmarkar/Khachiyanalgorithm

Theorem Zankl and Middeldorp, 2007

KBO{0,1,...,B} termination (B∈N) is decidable viaSAT/PBCencodings

Theorem

KBO_R

>0 termination is decidable viaSMT(linear arithmetic) encoding

Theorem Dick, Kalmus, and Martin, 1990

KBO_R>0 termination is decidable by MCD

Theorem Korovin and Voronkov, 2001, 2003

KBO_R>0 termination is decidable by Karmarkar/Khachiyanalgorithm

Theorem Zankl and Middeldorp, 2007

KBO{0,1,...,B} termination (B∈N) is decidable viaSAT/PBCencodings

Theorem

KBO_R

>0 termination is decidable viaSMT(linear arithmetic) encoding

Theorem Dick, Kalmus, and Martin, 1990

KBO_R>0 termination is decidable by MCD

Theorem Korovin and Voronkov, 2001, 2003

KBO_R>0 termination is decidable by Karmarkar/Khachiyanalgorithm

Theorem Zankl and Middeldorp, 2007

KBO{0,1,...,B} termination (B∈N) is decidable viaSAT/PBCencodings

Theorem

KBO_R

>0 termination is decidable viaSMT(linear arithmetic) encoding

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0

PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB 60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0 PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB

60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0 PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB 60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0 PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB 60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0 PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB 60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0 PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB 60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0 PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB 60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0 PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB 60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0 PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB 60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Experiments

test-bed: 1381TRSsfrom Termination Problem Data Base 4.0 PC: 8 dual-core AMD Opteron 885, 2.6 GHz, 64 GB 60 seconds timeout

method(B) total time(sec) #success #timeout

MCD 444 102 7

simplex 370 105 4

SAT/PBC(4) 31/90 104/104 0/0

SAT/PBC(8) 32/93 106/106 0/0

SAT/PBC(16) 34/100 107/107 0/0

SAT/PBC(1024) 351/187 107/107 3/1

SMT 26 107 0

Conclusion

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N^4N+1 Ris KBO_R>0 terminating

⇐⇒ Ris KBO_Nterminating Korovin and Voronkov

⇐⇒ Ris KBO{0,1,...,B} terminating this talk

CONCLUSION

finite characterization of KBO orientability use SMT solver to automate

FUTURE WORK

find optimalB

Conclusion

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N^4N+1 Ris KBO_R>0 terminating

⇐⇒ Ris KBO_Nterminating Korovin and Voronkov

⇐⇒ Ris KBO{0,1,...,B} terminating this talk

CONCLUSION

finite characterization of KBO orientability use SMT solver to automate

FUTURE WORK

find optimalB

Thank You for Your Attention