YES Left Termination proof of ../tpdb/LP/talp/maria/grammar.pl
Left Termination of the query pattern w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PredefinedPredicateTransformerProof

Clauses:

goal :- ','(np(S1, S2, S), verb(S2, S3, S)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), verb(S1, [], Meaning)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), ','(verb(S1, S2, Meaning), =(S2, []))).
np(Si, So, S) :- ','(det(Si, St, T), ','(noun(St, So, N), comb(T, N, S))).
comb(a, -(N, s), s(s, N, V)).
comb(the, -(N, P), s(P, N, V)).
det(.(a, S), S, a).
det(.(the, S), S, the).
noun(.(book, S), S, -(book, s)).
noun(.(books, S), S, -(book, p)).
noun(.(box, S), S, -(box, s)).
noun(.(boxes, S), S, -(box, p)).
verb(.(falls, So), So, s(s, N, fall)).
verb(.(fall, So), So, s(p, N, fall)).
verb(.(flies, So), So, s(s, N, fly)).
verb(.(fly, So), So, s(p, N, fly)).

Queries:

goal().

Added definitions of predefined predicates.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ PrologToPiTRSProof

Clauses:

goal :- ','(np(S1, S2, S), verb(S2, S3, S)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), verb(S1, [], Meaning)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), ','(verb(S1, S2, Meaning), =(S2, []))).
np(Si, So, S) :- ','(det(Si, St, T), ','(noun(St, So, N), comb(T, N, S))).
comb(a, -(N, s), s(s, N, V)).
comb(the, -(N, P), s(P, N, V)).
det(.(a, S), S, a).
det(.(the, S), S, the).
noun(.(book, S), S, -(book, s)).
noun(.(books, S), S, -(book, p)).
noun(.(box, S), S, -(box, s)).
noun(.(boxes, S), S, -(box, p)).
verb(.(falls, So), So, s(s, N, fall)).
verb(.(fall, So), So, s(p, N, fall)).
verb(.(flies, So), So, s(s, N, fly)).
verb(.(fly, So), So, s(p, N, fly)).
=(X, X).

Queries:

goal().

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
np_in: (f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

goal_in_ → U1_(np_in_aaa(S1, S2, S))
np_in_aaa(Si, So, S) → U7_aaa(Si, So, S, det_in_aaa(Si, St, T))
det_in_aaa(.(a, S), S, a) → det_out_aaa(.(a, S), S, a)
det_in_aaa(.(the, S), S, the) → det_out_aaa(.(the, S), S, the)
U7_aaa(Si, So, S, det_out_aaa(Si, St, T)) → U8_aaa(Si, So, S, T, noun_in_aaa(St, So, N))
noun_in_aaa(.(book, S), S, -(book, s)) → noun_out_aaa(.(book, S), S, -(book, s))
noun_in_aaa(.(books, S), S, -(book, p)) → noun_out_aaa(.(books, S), S, -(book, p))
noun_in_aaa(.(box, S), S, -(box, s)) → noun_out_aaa(.(box, S), S, -(box, s))
noun_in_aaa(.(boxes, S), S, -(box, p)) → noun_out_aaa(.(boxes, S), S, -(box, p))
U8_aaa(Si, So, S, T, noun_out_aaa(St, So, N)) → U9_aaa(Si, So, S, comb_in_gga(T, N, S))
comb_in_gga(a, -(N, s), s(s, N, V)) → comb_out_gga(a, -(N, s), s(s, N, V))
comb_in_gga(the, -(N, P), s(P, N, V)) → comb_out_gga(the, -(N, P), s(P, N, V))
U9_aaa(Si, So, S, comb_out_gga(T, N, S)) → np_out_aaa(Si, So, S)
U1_(np_out_aaa(S1, S2, S)) → U2_(verb_in_aag(S2, S3, S))
verb_in_aag(.(falls, So), So, s(s, N, fall)) → verb_out_aag(.(falls, So), So, s(s, N, fall))
verb_in_aag(.(fall, So), So, s(p, N, fall)) → verb_out_aag(.(fall, So), So, s(p, N, fall))
verb_in_aag(.(flies, So), So, s(s, N, fly)) → verb_out_aag(.(flies, So), So, s(s, N, fly))
verb_in_aag(.(fly, So), So, s(p, N, fly)) → verb_out_aag(.(fly, So), So, s(p, N, fly))
U2_(verb_out_aag(S2, S3, S)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
np_in_aaa(x1, x2, x3)  =  np_in_aaa
U7_aaa(x1, x2, x3, x4)  =  U7_aaa(x4)
det_in_aaa(x1, x2, x3)  =  det_in_aaa
det_out_aaa(x1, x2, x3)  =  det_out_aaa(x3)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x4, x5)
noun_in_aaa(x1, x2, x3)  =  noun_in_aaa
noun_out_aaa(x1, x2, x3)  =  noun_out_aaa(x3)
U9_aaa(x1, x2, x3, x4)  =  U9_aaa(x4)
comb_in_gga(x1, x2, x3)  =  comb_in_gga(x1, x2)
a  =  a
-(x1, x2)  =  -(x1, x2)
s  =  s
comb_out_gga(x1, x2, x3)  =  comb_out_gga(x3)
s(x1, x2, x3)  =  s(x1, x2)
the  =  the
np_out_aaa(x1, x2, x3)  =  np_out_aaa(x3)
U2_(x1)  =  U2_(x1)
verb_in_aag(x1, x2, x3)  =  verb_in_aag(x3)
verb_out_aag(x1, x2, x3)  =  verb_out_aag
p  =  p
goal_out_  =  goal_out_

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

goal_in_ → U1_(np_in_aaa(S1, S2, S))
np_in_aaa(Si, So, S) → U7_aaa(Si, So, S, det_in_aaa(Si, St, T))
det_in_aaa(.(a, S), S, a) → det_out_aaa(.(a, S), S, a)
det_in_aaa(.(the, S), S, the) → det_out_aaa(.(the, S), S, the)
U7_aaa(Si, So, S, det_out_aaa(Si, St, T)) → U8_aaa(Si, So, S, T, noun_in_aaa(St, So, N))
noun_in_aaa(.(book, S), S, -(book, s)) → noun_out_aaa(.(book, S), S, -(book, s))
noun_in_aaa(.(books, S), S, -(book, p)) → noun_out_aaa(.(books, S), S, -(book, p))
noun_in_aaa(.(box, S), S, -(box, s)) → noun_out_aaa(.(box, S), S, -(box, s))
noun_in_aaa(.(boxes, S), S, -(box, p)) → noun_out_aaa(.(boxes, S), S, -(box, p))
U8_aaa(Si, So, S, T, noun_out_aaa(St, So, N)) → U9_aaa(Si, So, S, comb_in_gga(T, N, S))
comb_in_gga(a, -(N, s), s(s, N, V)) → comb_out_gga(a, -(N, s), s(s, N, V))
comb_in_gga(the, -(N, P), s(P, N, V)) → comb_out_gga(the, -(N, P), s(P, N, V))
U9_aaa(Si, So, S, comb_out_gga(T, N, S)) → np_out_aaa(Si, So, S)
U1_(np_out_aaa(S1, S2, S)) → U2_(verb_in_aag(S2, S3, S))
verb_in_aag(.(falls, So), So, s(s, N, fall)) → verb_out_aag(.(falls, So), So, s(s, N, fall))
verb_in_aag(.(fall, So), So, s(p, N, fall)) → verb_out_aag(.(fall, So), So, s(p, N, fall))
verb_in_aag(.(flies, So), So, s(s, N, fly)) → verb_out_aag(.(flies, So), So, s(s, N, fly))
verb_in_aag(.(fly, So), So, s(p, N, fly)) → verb_out_aag(.(fly, So), So, s(p, N, fly))
U2_(verb_out_aag(S2, S3, S)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
np_in_aaa(x1, x2, x3)  =  np_in_aaa
U7_aaa(x1, x2, x3, x4)  =  U7_aaa(x4)
det_in_aaa(x1, x2, x3)  =  det_in_aaa
det_out_aaa(x1, x2, x3)  =  det_out_aaa(x3)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x4, x5)
noun_in_aaa(x1, x2, x3)  =  noun_in_aaa
noun_out_aaa(x1, x2, x3)  =  noun_out_aaa(x3)
U9_aaa(x1, x2, x3, x4)  =  U9_aaa(x4)
comb_in_gga(x1, x2, x3)  =  comb_in_gga(x1, x2)
a  =  a
-(x1, x2)  =  -(x1, x2)
s  =  s
comb_out_gga(x1, x2, x3)  =  comb_out_gga(x3)
s(x1, x2, x3)  =  s(x1, x2)
the  =  the
np_out_aaa(x1, x2, x3)  =  np_out_aaa(x3)
U2_(x1)  =  U2_(x1)
verb_in_aag(x1, x2, x3)  =  verb_in_aag(x3)
verb_out_aag(x1, x2, x3)  =  verb_out_aag
p  =  p
goal_out_  =  goal_out_


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GOAL_IN_ → U1_1(np_in_aaa(S1, S2, S))
GOAL_IN_ → NP_IN_AAA(S1, S2, S)
NP_IN_AAA(Si, So, S) → U7_AAA(Si, So, S, det_in_aaa(Si, St, T))
NP_IN_AAA(Si, So, S) → DET_IN_AAA(Si, St, T)
U7_AAA(Si, So, S, det_out_aaa(Si, St, T)) → U8_AAA(Si, So, S, T, noun_in_aaa(St, So, N))
U7_AAA(Si, So, S, det_out_aaa(Si, St, T)) → NOUN_IN_AAA(St, So, N)
U8_AAA(Si, So, S, T, noun_out_aaa(St, So, N)) → U9_AAA(Si, So, S, comb_in_gga(T, N, S))
U8_AAA(Si, So, S, T, noun_out_aaa(St, So, N)) → COMB_IN_GGA(T, N, S)
U1_1(np_out_aaa(S1, S2, S)) → U2_1(verb_in_aag(S2, S3, S))
U1_1(np_out_aaa(S1, S2, S)) → VERB_IN_AAG(S2, S3, S)

The TRS R consists of the following rules:

goal_in_ → U1_(np_in_aaa(S1, S2, S))
np_in_aaa(Si, So, S) → U7_aaa(Si, So, S, det_in_aaa(Si, St, T))
det_in_aaa(.(a, S), S, a) → det_out_aaa(.(a, S), S, a)
det_in_aaa(.(the, S), S, the) → det_out_aaa(.(the, S), S, the)
U7_aaa(Si, So, S, det_out_aaa(Si, St, T)) → U8_aaa(Si, So, S, T, noun_in_aaa(St, So, N))
noun_in_aaa(.(book, S), S, -(book, s)) → noun_out_aaa(.(book, S), S, -(book, s))
noun_in_aaa(.(books, S), S, -(book, p)) → noun_out_aaa(.(books, S), S, -(book, p))
noun_in_aaa(.(box, S), S, -(box, s)) → noun_out_aaa(.(box, S), S, -(box, s))
noun_in_aaa(.(boxes, S), S, -(box, p)) → noun_out_aaa(.(boxes, S), S, -(box, p))
U8_aaa(Si, So, S, T, noun_out_aaa(St, So, N)) → U9_aaa(Si, So, S, comb_in_gga(T, N, S))
comb_in_gga(a, -(N, s), s(s, N, V)) → comb_out_gga(a, -(N, s), s(s, N, V))
comb_in_gga(the, -(N, P), s(P, N, V)) → comb_out_gga(the, -(N, P), s(P, N, V))
U9_aaa(Si, So, S, comb_out_gga(T, N, S)) → np_out_aaa(Si, So, S)
U1_(np_out_aaa(S1, S2, S)) → U2_(verb_in_aag(S2, S3, S))
verb_in_aag(.(falls, So), So, s(s, N, fall)) → verb_out_aag(.(falls, So), So, s(s, N, fall))
verb_in_aag(.(fall, So), So, s(p, N, fall)) → verb_out_aag(.(fall, So), So, s(p, N, fall))
verb_in_aag(.(flies, So), So, s(s, N, fly)) → verb_out_aag(.(flies, So), So, s(s, N, fly))
verb_in_aag(.(fly, So), So, s(p, N, fly)) → verb_out_aag(.(fly, So), So, s(p, N, fly))
U2_(verb_out_aag(S2, S3, S)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
np_in_aaa(x1, x2, x3)  =  np_in_aaa
U7_aaa(x1, x2, x3, x4)  =  U7_aaa(x4)
det_in_aaa(x1, x2, x3)  =  det_in_aaa
det_out_aaa(x1, x2, x3)  =  det_out_aaa(x3)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x4, x5)
noun_in_aaa(x1, x2, x3)  =  noun_in_aaa
noun_out_aaa(x1, x2, x3)  =  noun_out_aaa(x3)
U9_aaa(x1, x2, x3, x4)  =  U9_aaa(x4)
comb_in_gga(x1, x2, x3)  =  comb_in_gga(x1, x2)
a  =  a
-(x1, x2)  =  -(x1, x2)
s  =  s
comb_out_gga(x1, x2, x3)  =  comb_out_gga(x3)
s(x1, x2, x3)  =  s(x1, x2)
the  =  the
np_out_aaa(x1, x2, x3)  =  np_out_aaa(x3)
U2_(x1)  =  U2_(x1)
verb_in_aag(x1, x2, x3)  =  verb_in_aag(x3)
verb_out_aag(x1, x2, x3)  =  verb_out_aag
p  =  p
goal_out_  =  goal_out_
DET_IN_AAA(x1, x2, x3)  =  DET_IN_AAA
U9_AAA(x1, x2, x3, x4)  =  U9_AAA(x4)
U7_AAA(x1, x2, x3, x4)  =  U7_AAA(x4)
U2_1(x1)  =  U2_1(x1)
VERB_IN_AAG(x1, x2, x3)  =  VERB_IN_AAG(x3)
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x4, x5)
NP_IN_AAA(x1, x2, x3)  =  NP_IN_AAA
GOAL_IN_  =  GOAL_IN_
U1_1(x1)  =  U1_1(x1)
COMB_IN_GGA(x1, x2, x3)  =  COMB_IN_GGA(x1, x2)
NOUN_IN_AAA(x1, x2, x3)  =  NOUN_IN_AAA

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

GOAL_IN_ → U1_1(np_in_aaa(S1, S2, S))
GOAL_IN_ → NP_IN_AAA(S1, S2, S)
NP_IN_AAA(Si, So, S) → U7_AAA(Si, So, S, det_in_aaa(Si, St, T))
NP_IN_AAA(Si, So, S) → DET_IN_AAA(Si, St, T)
U7_AAA(Si, So, S, det_out_aaa(Si, St, T)) → U8_AAA(Si, So, S, T, noun_in_aaa(St, So, N))
U7_AAA(Si, So, S, det_out_aaa(Si, St, T)) → NOUN_IN_AAA(St, So, N)
U8_AAA(Si, So, S, T, noun_out_aaa(St, So, N)) → U9_AAA(Si, So, S, comb_in_gga(T, N, S))
U8_AAA(Si, So, S, T, noun_out_aaa(St, So, N)) → COMB_IN_GGA(T, N, S)
U1_1(np_out_aaa(S1, S2, S)) → U2_1(verb_in_aag(S2, S3, S))
U1_1(np_out_aaa(S1, S2, S)) → VERB_IN_AAG(S2, S3, S)

The TRS R consists of the following rules:

goal_in_ → U1_(np_in_aaa(S1, S2, S))
np_in_aaa(Si, So, S) → U7_aaa(Si, So, S, det_in_aaa(Si, St, T))
det_in_aaa(.(a, S), S, a) → det_out_aaa(.(a, S), S, a)
det_in_aaa(.(the, S), S, the) → det_out_aaa(.(the, S), S, the)
U7_aaa(Si, So, S, det_out_aaa(Si, St, T)) → U8_aaa(Si, So, S, T, noun_in_aaa(St, So, N))
noun_in_aaa(.(book, S), S, -(book, s)) → noun_out_aaa(.(book, S), S, -(book, s))
noun_in_aaa(.(books, S), S, -(book, p)) → noun_out_aaa(.(books, S), S, -(book, p))
noun_in_aaa(.(box, S), S, -(box, s)) → noun_out_aaa(.(box, S), S, -(box, s))
noun_in_aaa(.(boxes, S), S, -(box, p)) → noun_out_aaa(.(boxes, S), S, -(box, p))
U8_aaa(Si, So, S, T, noun_out_aaa(St, So, N)) → U9_aaa(Si, So, S, comb_in_gga(T, N, S))
comb_in_gga(a, -(N, s), s(s, N, V)) → comb_out_gga(a, -(N, s), s(s, N, V))
comb_in_gga(the, -(N, P), s(P, N, V)) → comb_out_gga(the, -(N, P), s(P, N, V))
U9_aaa(Si, So, S, comb_out_gga(T, N, S)) → np_out_aaa(Si, So, S)
U1_(np_out_aaa(S1, S2, S)) → U2_(verb_in_aag(S2, S3, S))
verb_in_aag(.(falls, So), So, s(s, N, fall)) → verb_out_aag(.(falls, So), So, s(s, N, fall))
verb_in_aag(.(fall, So), So, s(p, N, fall)) → verb_out_aag(.(fall, So), So, s(p, N, fall))
verb_in_aag(.(flies, So), So, s(s, N, fly)) → verb_out_aag(.(flies, So), So, s(s, N, fly))
verb_in_aag(.(fly, So), So, s(p, N, fly)) → verb_out_aag(.(fly, So), So, s(p, N, fly))
U2_(verb_out_aag(S2, S3, S)) → goal_out_

The argument filtering Pi contains the following mapping:
goal_in_  =  goal_in_
U1_(x1)  =  U1_(x1)
np_in_aaa(x1, x2, x3)  =  np_in_aaa
U7_aaa(x1, x2, x3, x4)  =  U7_aaa(x4)
det_in_aaa(x1, x2, x3)  =  det_in_aaa
det_out_aaa(x1, x2, x3)  =  det_out_aaa(x3)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x4, x5)
noun_in_aaa(x1, x2, x3)  =  noun_in_aaa
noun_out_aaa(x1, x2, x3)  =  noun_out_aaa(x3)
U9_aaa(x1, x2, x3, x4)  =  U9_aaa(x4)
comb_in_gga(x1, x2, x3)  =  comb_in_gga(x1, x2)
a  =  a
-(x1, x2)  =  -(x1, x2)
s  =  s
comb_out_gga(x1, x2, x3)  =  comb_out_gga(x3)
s(x1, x2, x3)  =  s(x1, x2)
the  =  the
np_out_aaa(x1, x2, x3)  =  np_out_aaa(x3)
U2_(x1)  =  U2_(x1)
verb_in_aag(x1, x2, x3)  =  verb_in_aag(x3)
verb_out_aag(x1, x2, x3)  =  verb_out_aag
p  =  p
goal_out_  =  goal_out_
DET_IN_AAA(x1, x2, x3)  =  DET_IN_AAA
U9_AAA(x1, x2, x3, x4)  =  U9_AAA(x4)
U7_AAA(x1, x2, x3, x4)  =  U7_AAA(x4)
U2_1(x1)  =  U2_1(x1)
VERB_IN_AAG(x1, x2, x3)  =  VERB_IN_AAG(x3)
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x4, x5)
NP_IN_AAA(x1, x2, x3)  =  NP_IN_AAA
GOAL_IN_  =  GOAL_IN_
U1_1(x1)  =  U1_1(x1)
COMB_IN_GGA(x1, x2, x3)  =  COMB_IN_GGA(x1, x2)
NOUN_IN_AAA(x1, x2, x3)  =  NOUN_IN_AAA

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 0 SCCs with 10 less nodes.