Huge bug in recursive aggregates

[Bart Bogaerts]

The attached file (with any of the two lines of which one is outcommented) should have exactly one model, namely one in which no company controls another company.

However, depending on which line I use, I get 8 models or 1 wrong model.

This is because recursive aggregates are not handled very well, either in the grounder or in the solver...

[Bart Bogaerts]

Ik verdenk IDP ervan om foute transformaties te doen, zoals sum >= 5 vervangen door ~sum < 5 wat logisch equivalent lijkt, maar de semantiek van aggregaten niet bewaart!

[Ingmar Dasseville]

no attached file ;)

[Bart Bogaerts]

Yes, there is :p

[Ingmar Dasseville]

de twee lijnen zijn identiek?

[Bart Bogaerts]

Een van de twee moet zijn

...>=5

de andere

...>5

[Ingmar Dasseville]

Is de semantiek ergens beschreven? Nu ik er over nadenk weet ik niet zo goed hoe ik die moet interpreteren. Wat verwacht je bvb van deze theorie?

vocabulary V{
    type T isa int
    a(T)
    b(T)
}

theory T:V{

    {
        b(1).
        b(2).
        ∀x: b(x) ← a(x).
        ∀x: a(x) ← sum{y[T] : b(y) : y}-2000≤ x.

    }
}

structure S:V{
    T = {1..20}

}

Geeft momenteel unsat. Maar mijn redenering voor een definitie is wel dat, als er een fixpoint is, dat er ook altijd een oplossing uitkomt in stable semantics

[Bart Bogaerts]

Die is niet monotoon, dus dat is complexer! Monotone dingen begrijpen (en juist hebben) is moeilijk genoeg

De semantiek is beschreven in enkele papers van Nikolai Pelov...

Wat je redenering over Stable semantics betreft: dit klopt niet.

vb:

p:- not p, q

q :- not q, p

heeft als fixpoint {p,q}, maar hefet geen stable fixpoints