1. KRR Avatar KRR
  2. software
  3. IDP
  4. Issues

Push quantifiers down is too strict.

Issue #597 new
Broes De Cat created an issue

Sergey's example:

P(x) <- ?y: Q(x) & R(x,y) then y is not pushed down, but should.

Comments (2)

  1. Broes De Cat reporter

    Other example: Value(f,va,vb,vc) <- f > 1 & FOp(f) = o & FLeft(f) = fl & FRight(f) = fr & Value(fl,va,vb,vl) & Value(fr,va,vb,vr) & TT(o,vl,vr,vc).

    Current settings: grounding of 4 million atoms. Remove break condition (bsubf->isConjWithSign() != qf->isUniv()): 1.1 million atoms. Manual reordering (below): 70.000 atoms!!!

    / & ?vr: (?fr: FRight(f) = fr & Value(fr,va,vb,vr)) & ?vl: (?fl: FLeft(f) = fl & Value(fl,va,vb,vl)) & ?o: FOp(f) = o & TT(o,vl,vr,vc)./

  3. Log in to comment
Assignee
–
Type
enhancement
Priority
major
Status
new
Component
–
Version
–
Votes
0
Watchers
1
Jira: the preferred issue tracker for Bitbucket. Join the team!