• 検索結果がありません。

# KBO Orientability

N/A
N/A
Protected

シェア "KBO Orientability"

Copied!
102
0
0

(1)

## KBO Orientability

### Aart Middeldorp

† Japan Advanced Institute of Science and Technology

‡ University of Innsbruck

(2)

### Reference

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

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

(3)

### 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

(4)

### 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

(5)

### 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)

(6)

### Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1Rt2R· · ·

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, ...)

(7)

### Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1Rt2R· · ·

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, ...)

(8)

### Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1Rt2R· · ·

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, ...)

(9)

### Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1Rt2R· · ·

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, ...)

(10)

### Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1Rt2R· · ·

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, ...)

(11)

### Termination

Definition

TRSRis terminatingif there is no infinite rewrite sequence t1Rt2R· · ·

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, ...)

(12)

### 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) =

(w0 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

(13)

### 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) =

(w0 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

(14)

### 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) =

(w0 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

(15)

### 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) =

(w0 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

(16)

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=fn(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

(17)

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=fn(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

(18)

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=fn(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

(19)

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=fn(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

(20)

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=fn(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

(21)

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=fn(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

(22)

Definition

letX ⊆R>0. TRSRisKBOX terminatingif

∃ precedence>

∃ admissible weight function(w, w0)∈XF×X such thatl >kborfor alll→r∈ R

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBON terminating

(23)

Definition

letX ⊆R>0. TRSRisKBOX terminatingif

∃ precedence>

∃ admissible weight function(w, w0)∈XF×X such thatl >kborfor alll→r∈ R

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBON terminating

(24)

## Quiz

(25)

### Example I

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

is KBONterminating ? — yes

Proof

take precedencea>band weight function w(a) =

?3

w(b) =

?2

w0= 1

Proof

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

?13

w(b) =

?8

w0= 1

(26)

### Example I

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

is KBONterminating ?

—yes

Proof

take precedencea>band weight function w(a) =

?3

w(b) =

?2

w0= 1

Proof

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

?13

w(b) =

?8

w0= 1

(27)

### Example I

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

is KBONterminating ? — yes

Proof

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

3

w(b) = ?

2

w0= 1

Proof

another solution: take precedence>=∅and weight function

w(a) =

?13

w(b) =

?8

w0= 1

(28)

### Example I

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

is KBONterminating ? — yes

Proof

take precedencea>band weight function w(a) =

?

3 w(b) =

?

2 w0= 1

Proof

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

?13

w(b) =

?8

w0= 1

(29)

### Example I

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

is KBONterminating ? — yes

Proof

take precedencea>band weight function w(a) =

?

3 w(b) =

?

2 w0= 1

Proof

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

13

w(b) = ?

8

w0= 1

(30)

### Example I

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

is KBONterminating ? — yes

Proof

take precedencea>band weight function w(a) =

?

3 w(b) =

?

2 w0= 1

Proof

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

?

13 w(b) =

?

8 w0= 1

(31)

### Example II

TRSR

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

—no

(32)

### Example II

TRSR

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

(33)

## History of KBO

(34)

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBON terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBOR>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBOR>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBONterminating ⇐⇒ it is KBOR>0 terminating

KBOR>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

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

(35)

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBON terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBOR>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBOR>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBONterminating ⇐⇒ it is KBOR>0 terminating

KBOR>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

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

(36)

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBON terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBOR>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBOR>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBONterminating ⇐⇒ it is KBOR>0 terminating

KBOR>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

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

(37)

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBON terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBOR>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBOR>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBONterminating ⇐⇒ it is KBOR>0 terminating

KBOR>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

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

(38)

Theorem Knuth and Bendix, 1970

TRS is terminating if it is KBON terminating

Theorem Dershowitz, 1979

TRS is terminating if it is KBOR>0 terminating

Theorem Dick, Kalmus, and Martin, 1990

KBOR>0 termination isdecidablewithin exponential time

Theorem Korovin and Voronkov, 2001, 2003

TRS is KBONterminating ⇐⇒ it is KBOR>0 terminating

KBOR>0 termination is decidable withinpolynomial time

Theorem Zankl and Middeldorp, 2007

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

(39)

### This Talk

MAIN RESULT

for every TRSRandN =P

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

Ris KBONterminating ⇐⇒ Ris KBO{0,1,...,B} terminating where,B=N4N+1

OVERVIEW OF PROOF

Principal Solutions

MCD

Bound by Norm

(40)

### This Talk

MAIN RESULT

for every TRSRandN =P

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

Ris KBONterminating ⇐⇒ Ris KBO{0,1,...,B} terminating where,B=N4N+1

OVERVIEW OF PROOF

Principal Solutions

MCD

Bound by Norm

(41)

### This Talk

MAIN RESULT

for every TRSRandN =P

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

Ris KBONterminating ⇐⇒ Ris KBO{0,1,...,B} terminating where,B=N4N+1

OVERVIEW OF PROOF

Principal Solutions

MCD

Bound by Norm

(42)

### This Talk

MAIN RESULT

for every TRSRandN =P

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

Ris KBONterminating ⇐⇒ Ris KBO{0,1,...,B} terminating where,B=N4N+1

OVERVIEW OF PROOF

Principal Solutions

MCD

Bound by Norm

(43)

## Principal Solutions

(44)

### Example

given precedence, KBONproblem 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

(45)

### Example

given precedence, KBONproblem 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

(46)

### Example

given precedence, KBONproblem 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

(47)

### Principal Solutions

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

setI of KBO inequalities are of form

{ ~ai·~xi Ri 0 }i with Ri∈{>, >},~ai∈Zn,~x∈N

Definition

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

~

xissolutionofAI ifAI~x>0and~x∈Nn

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

Theorem

principal solution ofA always exists

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

(48)

### Principal Solutions

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

setI of KBO inequalities are of form

{ ~ai·~xi Ri 0 }i with Ri∈{>, >},~ai∈Zn,~x∈N

Definition

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

~

xissolutionofAI ifAI~x>0and~x∈Nn

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

Theorem

principal solution ofA always exists

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

(49)

### Principal Solutions

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

setI of KBO inequalities are of form

{ ~ai·~xi Ri 0 }i with Ri∈{>, >},~ai∈Zn,~x∈N

Definition

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

~

xissolutionofAI ifAI~x>0and~x∈Nn

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

Theorem

principal solution ofA always exists

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

(50)

### Principal Solutions

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

setI of KBO inequalities are of form

{ ~ai·~xi Ri 0 }i with Ri∈{>, >},~ai∈Zn,~x∈N

Definition

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

~

xissolutionofAI ifAI~x>0and~x∈Nn

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

Theorem

principal solution ofA always exists

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

(51)

### Principal Solutions

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

setI of KBO inequalities are of form

{ ~ai·~xi Ri 0 }i with Ri∈{>, >},~ai∈Zn,~x∈N

Definition

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

~

xissolutionofAI ifAI~x>0and~x∈Nn

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

Theorem

principal solution ofA always exists

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

(52)

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 solutionofAI and satisfiesI hence I issolvable

(53)

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 solutionofAI and satisfiesI hence I issolvable

(54)

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 solutionofAI and satisfiesI hence Iis solvable

(55)

### 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

(56)

### 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

(57)

### 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

(58)

### 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

(59)

### 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

(60)

## MCD: Method of Complete Description

(61)

### MCD

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

form×nmatrixA and06i6m SiA=

(En ifi= 0 Si−1A (~aiSi−1A )κ otherwise

sum of all column vectors of SmA is denoted by~sA

Theorem

~sAis principal solutionofA

(62)

### MCD

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

form×nmatrixA and06i6m SiA=

(En ifi= 0 Si−1A (~aiSi−1A )κ otherwise

sum of all column vectors of SmA is denoted by~sA

Theorem

~sAis principal solutionofA

(63)

### MCD

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

form×nmatrixA and06i6m SiA=

(En ifi= 0 Si−1A (~aiSi−1A )κ otherwise

sum of all column vectors ofSAmis denoted by~sA

Theorem

~sAis principal solutionofA

(64)

### MCD

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

form×nmatrixA and06i6m SiA=

(En ifi= 0 Si−1A (~aiSi−1A )κ otherwise

sum of all column vectors ofSAmis denoted by~sA

Theorem

~sAis principal solutionofA

(65)

### Example

I=

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

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

AI =

2 −3

−3 5

performing MCD S0AI =

1 0 0 1

S1AI =S0AI((2 −3)S0AI)κ= 1 3

0 2

S2AI =S1AI((−3 5)S1AI)κ=

3 10 2 6

we obtain principal solution

~ sAI =

3 2

+ 10

6

= 13

8

which satisfiesI. henceI is solvable

(66)

### Example

I=

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

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

AI =

2 −3

−3 5

performing MCD

S0AI = 1 0

0 1

S1AI =S0AI((2 −3)S0AI)κ= 1 3

0 2

S2AI =S1AI((−3 5)S1AI)κ=

3 10 2 6

we obtain principal solution

~ sAI =

3 2

+ 10

6

= 13

8

which satisfiesI. henceI is solvable

(67)

### Example

I=

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

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

AI =

2 −3

−3 5

performing MCD S0AI =

1 0 0 1

S1AI =S0AI((2 −3)S0AI)κ= 1 3

0 2

S2AI =S1AI((−3 5)S1AI)κ=

3 10 2 6

we obtain principal solution

~ sAI =

3 2

+ 10

6

= 13

8

which satisfiesI. henceI is solvable

(68)

### Example

I=

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

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

AI =

2 −3

−3 5

performing MCD S0AI =

1 0 0 1

S1AI =S0AI((2 −3)S0AI)κ= 1 3

0 2

S2AI =S1AI((−3 5)S1AI)κ=

3 10 2 6

we obtain principal solution

~sAI = 3

2

+ 10

6

= 13

8

which satisfiesI. henceI is solvable

(69)

### Example

I=

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

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

AI =

2 −3

−3 5

performing MCD S0AI =

1 0 0 1

S1AI =S0AI((2 −3)S0AI)κ= 1 3

0 2

S2AI =S1AI((−3 5)S1AI)κ=

3 10 2 6

we obtain principal solution

~sAI = 3

2

+ 10

6

= 13

8

(70)

## Bound by Norm

(71)

### MCD

(a1, . . . , an)κ= (~ei|ai>0) ++(aj~ei−ai~ej|ai<0, aj >0)

form×nmatrixA and06i6m SiA=

(En ifi= 0 Si−1A (~aiSi−1A )κ otherwise

sum of all column vectors ofSAmis denoted by~sA

GOAL

bound~sA∈ {0,1, . . . , B}n

APPROACH

definenormk · kto calculatek~sAIk withB=k~sAIk

(72)

### MCD

(a1, . . . , an)κ= (~ei|ai>0) ++(aj~ei−ai~ej|ai<0, aj >0)

form×nmatrixA and06i6m SiA=

(En ifi= 0 Si−1A (~aiSi−1A )κ otherwise

sum of all column vectors ofSAmis denoted by~sA

GOAL

bound~sA∈ {0,1, . . . , B}n

APPROACH

definenormk · kto calculatek~sAIk withB=k~sAIk

(73)

### MCD

(a1, . . . , an)κ= (~ei|ai>0) ++(aj~ei−ai~ej|ai<0, aj >0)

form×nmatrixA and06i6m SiA=

(En ifi= 0 Si−1A (~aiSi−1A )κ otherwise

sum of all column vectors ofSAmis denoted by~sA

GOAL

bound~sA∈ {0,1, . . . , B}n

APPROACH

definenormk · kto calculatek~sAIk withB=k~sAIk

(74)

### Norm

Definition

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

Lemma

for everym×nmatrixAandn×pmatrixB kaκk=kak

kABk6nkAkkBk

(a1, . . . , an)κ isn×kmatrix withk6n2. SAi ism×kmatrix withk6n2i.

kSiAk6(2mkAk)2i−1 k~sAk6n2m·(2mkAk)2m−1

(75)

### Norm

Definition

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

Lemma

for everym×nmatrixAandn×pmatrixB kaκk=kak

kABk6nkAkkBk

(a1, . . . , an)κ isn×kmatrix withk6n2. SAi ism×kmatrix withk6n2i.

kSiAk6(2mkAk)2i−1 k~sAk6n2m·(2mkAk)2m−1

(76)

### Norm

Definition

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

Lemma

for everym×nmatrixAandn×pmatrixB kaκk=kak

kABk6nkAkkBk

(a1, . . . , an)κ isn×kmatrix withk6n2. SAi ism×kmatrix withk6n2i.

kSiAk6(2mkAk)2i−1 k~sAk6n2m·(2mkAk)2m−1

(77)

### Norm

Definition

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

Lemma

for everym×nmatrixAandn×pmatrixB kaκk=kak

kABk6nkAkkBk

(a1, . . . , an)κ isn×kmatrix withk6n2. SAi ism×kmatrix withk6n2i.

kSiAk6(2mkAk)2i−1 k~sAk6n2m·(2mkAk)2m−1

(78)

### Norm

Definition

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

Lemma

for everym×nmatrixAandn×pmatrixB kaκk=kak

kABk6nkAkkBk

(a1, . . . , an)κ isn×kmatrix withk6n2. SAi ism×kmatrix withk6n2i.

kSiAk6(2mkAk)2i−1 k~sAk6n2m·(2mkAk)2m−1

(79)

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~sAIk6N4N+1:=B thus,

~sAI ∈ {0,1, . . . , B}n

(80)

### Main Result

Theorem

Ris KBONterminating ⇐⇒ Ris KBO{0,1,...,B}terminating where,B=N4N+1

Corollary

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

(81)

### Main Result

Theorem

Ris KBONterminating ⇐⇒ Ris KBO{0,1,...,B}terminating where,B=N4N+1

Corollary

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

(82)

### Summary

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N4N+1 Ris KBOR

>0 terminating

⇐⇒ Ris KBONterminating Korovin and Voronkov

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

theoretical interest of decidability issue is more or less closed

(83)

### Summary

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N4N+1 Ris KBOR

>0 terminating

⇐⇒ Ris KBONterminating Korovin and Voronkov

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

theoretical interest of decidability issue is more or less closed

(84)

### Summary

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N4N+1 Ris KBOR

>0 terminating

⇐⇒ Ris KBONterminating Korovin and Voronkov

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

theoretical interest of decidability issue is more or less closed

(85)

## Automation

(86)

Theorem Dick, Kalmus, and Martin, 1990

KBOR>0 termination is decidable by MCD

Theorem Korovin and Voronkov, 2001, 2003

KBOR>0 termination is decidable by Karmarkar/Khachiyanalgorithm

Theorem Zankl and Middeldorp, 2007

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

Theorem

KBOR

>0 termination is decidable viaSMT(linear arithmetic) encoding

(87)

Theorem Dick, Kalmus, and Martin, 1990

KBOR>0 termination is decidable by MCD

Theorem Korovin and Voronkov, 2001, 2003

KBOR>0 termination is decidable by Karmarkar/Khachiyanalgorithm

Theorem Zankl and Middeldorp, 2007

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

Theorem

KBOR

>0 termination is decidable viaSMT(linear arithmetic) encoding

(88)

Theorem Dick, Kalmus, and Martin, 1990

KBOR>0 termination is decidable by MCD

Theorem Korovin and Voronkov, 2001, 2003

KBOR>0 termination is decidable by Karmarkar/Khachiyanalgorithm

Theorem Zankl and Middeldorp, 2007

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

Theorem

KBOR

>0 termination is decidable viaSMT(linear arithmetic) encoding

(89)

Theorem Dick, Kalmus, and Martin, 1990

KBOR>0 termination is decidable by MCD

Theorem Korovin and Voronkov, 2001, 2003

KBOR>0 termination is decidable by Karmarkar/Khachiyanalgorithm

Theorem Zankl and Middeldorp, 2007

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

Theorem

KBOR

>0 termination is decidable viaSMT(linear arithmetic) encoding

(90)

### 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

(91)

### 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

(92)

### 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

(93)

### 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

(94)

### 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

(95)

### 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

(96)

### 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

(97)

### 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

(98)

### 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

(99)

### 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

(100)

### Conclusion

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N4N+1 Ris KBOR>0 terminating

⇐⇒ Ris KBONterminating 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

(101)

### Conclusion

letRbe TRS,N =P

l→r∈R(|l|+|r|) + 1, andB=N4N+1 Ris KBOR>0 terminating

⇐⇒ Ris KBONterminating 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

(102)

## Thank You for Your Attention

A lemma of considerable generality is proved from which one can obtain inequali- ties of Popoviciu’s type involving norms in a Banach space and Gram determinants.. Key words

This paper deals with the modelling of complex sociopsychological games and recipro- cal feelings based on some conceptual developments of a new class of kinetic equations

By correcting these mistakes, we find that parameters of the spherical function are rational with respect to parameters of the (generalized principal series) representation.. As

Real elastic waves (earthquakes) propagate through many layers which do not necessarily lie in good order. Therefore, more general study, we extend the elastic wave equations

Tuncay, Oscillation theorems for a class of second order nonlinear differential equations with damping, Taiwanese Journal of Mathematics, 13 (2009), 1909- 1928..

de la CAL, Using stochastic processes for studying Bernstein-type operators, Proceedings of the Second International Conference in Functional Analysis and Approximation The-

[3] JI-CHANG KUANG, Applied Inequalities, 2nd edition, Hunan Education Press, Changsha, China, 1993J. FINK, Classical and New Inequalities in Analysis, Kluwer Academic

We describe a ﬁltration of Pic( L I ) in the last section as well as the proofs of some facts. We also discuss there the small objects in some local stable homotopy categories...