[Inference] Find (minimal) domain such that

[Bart Bogaerts]

A new inference which generates a full structure, from an unknown or partial domain.

[Bart Bogaerts]

Samenvatting van de discussie hierover:

Satisfiability checking:

Strategy A: for type t, add n domain elements where n is the number of existentially quantified subformula over t A model exists for the original theory iff it exists for this reduced theory.

Refinement A' of A: for each existentially quantified subformula over t, add a domainelement i=size(t) to t and introduce a skolem s_i and drop the quantification. The type of s_i is [1..i] A model exists for the original theory iff it exists for this reduced theory.

Strategy A: straightforward Cannot handle functions of arity >0 if infinite argument domains (needs unnesting of terms) or nested existential quantifications over infinite domains

Strategy A': Can make better use of congruence closure algorithms to check equalities of functions. Cannot handle nested existential quantifications over infinite domains.

A+A': Ground and solve iteratively, each time increasing the domain until a model is found: can decide satisfiability with a more reduced type, but not unsatisfiability.

Orthogonally on that: Lazy grounding with the current domain size, incrementally increasing as we go. Can decide unsatisfiability in some cases (of it is independent of the domain size)

[Bart Bogaerts]

Marc zijn herwerking:

Normale strategie voor gekend eindig type T = {d1,..,dn}

Ground(\exist x[T]:A[x]) -> Ground(A[d1]) v..v Ground(A[dn]) (eventueel met lazy grounding) Ground(\forall x[T]:A[x]) -> Ground(A[d1] &..& Ground(A[dn] (eventueel met lazy grounding)

Strategie met constraint vars/skolems voor gekend eindig type T = {d1,..,dn}:

Ground(\exist x[T]:A[x]) -> Ground(A[C]) & T(C) - C nieuwe skolem - dit vereist een solver met equality reasoning.

Ground(\forall x[T]:A[x]) -> Ground(A[d1] &..& Ground(A[dn]

Let wel, er zijn meer mogelijkheden in geval \forall. Bv. als A[x] van de vorm is B[x] v C[c] zodat B[x] alle domeinelementen d -of eventueel skolems- kan "genereren" waarvoor B[d] onwaar is, dan kun je gewoon wachten met A[d] te grounden totdat B[d] onwaar wordt. Er zitten hier allerleid stekels aan vast, maar het is wel interessant. Ik weet daar iets over van uit mijn Asystem tijd.

ONBEKEND TYPE.

Basisstrategie voor ongekend type T - we houden een dynamisch domein D_T bij. Initieel is het leeg. Potentiele elementen over d0,..., dn,... Voor elke di (i>0) uit D_T is er constraint : T(d_{i+1}) => T(d_i)

Ground(\exist x[T]:A[x]) -> T[d0]&Ground(A[d0]) v .. v T[dn]&Ground(A[dn]) indien D_T = {d0,..,d_n-1} ; bovendien voeg dn toe aan D_T. (lazy grounding toegelaten)

Ground(\forall x[T]:A[x]) -> Ground(A[d0])& ... & Ground(A[dn]) & T_A met D_T={d0,..,dn} T_A is een Tseitin die staat voor forall x[T\D_T]:A[x] Wanneer D_T uitgebreid wordt, moet T_A geground worden.

Strategie met constraint vars. Nog altijd een dynamisch domein D_T , en constraints T(di+1) => T(di).

Ground(\exist x[T]:A[x]) -> Ground(A[C]) & T(C) - C nieuwe skolem - solver met equality reasoning. En ik zou toevoegen: C =< max(C0,..,Cn-1)+1, met C0,..,Cn-1 de vroeger gecreeerde skolems.

Ground(\forall x[T]:A[x]) -> Ground(A[d0])& ... & Ground(A[dn]) & T_A met D_T={d0,..,dn} T_A is een Tseitin die staat voor forall x[T\D_T]:A[x] Wanneer D_T uitgebreid wordt, moet T_A geground worden.

[Broes De Cat]

Removing milestone: Later (automated comment)