are existential rules monotonic?

[balhoff]

I've been trying out VLog by following this tutorial: https://iccl.inf.tu-dresden.de/web/Rules_ECAI_Tutorial_2020/en

I'm using the VLog version in the Rulewerk console downloaded in the tutorial materials. I wrote a set of rules to infer something that I'm not easily able to do in OWL:

tooth(?X) :- molar_tooth(?X) .
part_of(?X, !T), tooth(!T) :- crown(?X) .
part_of(?X, !T), crown(!T) :- cingulum(?X) .

crown(?X), part_of(?X, !T), molar_tooth(!T) :- molar_crown(?X) .
molar_crown(?X) :- crown(?X), part_of(?X, ?T), molar_tooth(?T) .

cingulum(?X), part_of(?X, !T), molar_tooth(!T) :- molar_cingulum(?X) .
molar_cingulum(?X) :- cingulum(?X), part_of(?X, ?T), molar_tooth(?T) .

sameAs(?X, ?Y) :- cingulum(?C), tooth(?X), part_of(?C, ?X), tooth(?Y), part_of(?C, ?Y) .
part_of(?A, ?Z) :- part_of(?A, ?Y), sameAs(?Y, ?Z) .
sameAs(?Y, ?X) :- sameAs(?X, ?Y) .

part_of(?X, ?Z) :- part_of(?X, ?Y), part_of(?Y, ?Z) .

part_of_tooth(?X) :- tooth(?C), part_of(?X, ?C) .
part_of_molar_crown(?X) :- molar_crown(?C), part_of(?X, ?C) .
part_of_crown(?X) :- crown(?C), part_of(?X, ?C) .

molar_cingulum(mc1) .
%cingulum(mc2) .

If I load that file and run a query, I get one result:

rulewerk> @load "test.rls"
Loaded 1 new fact(s), 14 new rule(s), and 0 new datasource declaration(s).
rulewerk> @reason .
Loading and materializing inferences ...
... finished in 17ms (7ms CPU time).
rulewerk> @query part_of_molar_crown(?X) .
?X -> mc1
1 result(s) in 0ms. Results are sound and complete.

If I uncomment the last line, adding one fact, my query now returns zero results:

rulewerk> @load "test.rls"
Loaded 2 new fact(s), 14 new rule(s), and 0 new datasource declaration(s).
rulewerk> @reason .
Loading and materializing inferences ...
... finished in 7ms (5ms CPU time).
rulewerk> @query part_of_molar_crown(?X) .
0 result(s) in 0ms. Results are sound and complete.

Is this expected behavior?

[irina-dragoste]

This is clearly a bug. The expected answer is

@query part_of_molar_crown(?X) .
?X -> mc1

Existential rules can only be non-monotonic in the presence of negation, and the ruleset above does not contain any negation. Indeed, the restricted chase could lead to different materialisation results of different size depending on the rule application order, but all of them should be equivalent under a constant-preserving homomorphism (i.e. a homomorphism that only maps nulls created during reasoning). But this is also not the case in this example.

[CerielJacobs]

This issue actually appears to be very similar to issue #64. The problem again seems to be the filtering of results of the restricted chase in multihead rules. In Vlog, using the "--rewriteMultihead true" command line option works around the problem.

[irina-dragoste]

FYI, with the above commits, reasoning is now correct.