Improve definition-evaluation by grounding using approximation

[Broes De Cat]

Momenteel worden voor een regel sowieso alle mogelijke instantiaties van de variabelen gegenereerd die in zowel head als body voorkomen. Dit kan sterk verbeterd worden als volgt: voor symbolen waarvoor geen negatieve recursie mogelijk is: bodygen moet alleen de possibly true genereren van "forall bodyvars: body" dan moet de definitiegrounder een tabel bijhouden van alle heads die voor een bepaald symbool gegenereerd worden. Als alle regels geground zijn, moet de ct van dat symbool gemergd worden met de inversie van die tabel.

Dan zou vermoedelijk nqueens en bvb path() <- edge ... veel beter geground worden.

[Broes De Cat]

Extra voorbeeld:

waarbij Q gegeven is. Nu iterereert de grounder over het volledige domein van l, w en c.

[Bart Bogaerts]

Problemen hiermee: we moeten ervoor zorgen dat we geen lussen verliezen, enkele voorbeelden

{P(x) <- Q(x) }

P(x) <=> ~Q(x)

Q is gegeven. Dus het zou perfect mogelijk zijn dat P = ~Q wordt afgeleid door de bounds. In dat geval moet je de definitie grounden om correctheid te garanderen.

Wat we zouden kunnen doen is: P(x) <- \varphi(x) grounden door de pt voor varphi te gebruiken. Maar zelfs dat kan volgens mij misgaan

{P(x) <- ~Q(x) Q(x) <- ~P(x)}

Als Q altijd waar is zouden we de eerste regel niet grounden. Lus die verloren gaat...

Voorzichtigheid is dus geboden!!!!

[Broes De Cat]

Issue #253 was marked as a duplicate of this issue.