Skip to content

Fix Formula.simplify for entailments

Florian Sextl requested to merge florian.sextl/broom:fix_simplify into master

Problem

Formula.simplify should try to normalize variables, i.e. exchange equivalent ones in a fixed order. For example, the two following formulas get simplified quite differently just because the atomic formulas are ordered slightly different:

%l2 -(8)->%l3 & (%mF1:x_anch=%mF1:x) & (%l2=%mF1:x)

becomes

%mF1:x_anch -(8)->%l3 & (%mF1:x_anch=%mF1:x)

whereas

%l2 -(8)->%l3 & (%mF1:x_anch=%mF1:x) & (%mF1:x_anch=%l2)

becomes

%mF1:x -(8)->%l3 & (%mF1:x_anch=%mF1:x)

This difference in formulas leads to the following problem: The formulas

%l10 -(8)->%l9 & (%mF1:x_anch=%l10) & (%mF1:x=%l9)

%l10 -(8)->%l8 & (%mF1:x_anch=%mF1:x) & (%mF1:x_anch=%l10)

get simplified to

%mF1:x_anch -(8)->%mF1:x

%mF1:x -(8)->%l8 & (%mF1:x_anch=%mF1:x)

The simplified first formula entails the second one based on the implementation of the match rule (although the formal description in the paper would not allow this, is this also a bug, see below), whereas the original formula does not entail the other one.

With the change, the simplified formulas become

%mF1:x_anch -(8)->%mF1:x

%mF1:x_anch -(8)->%l8 & (%mF1:x_anch=%mF1:x)

which can not be matched for entailment.

Possible Match Bug

At https://pajda.fit.vutbr.cz/rogalew/broom/-/blob/master/src/biabduction/Abduction.ml#L926 the heads of the two spatial predicates are checked against each other modulo equality in both formulas, whereas the paper states that the rule might only be applied modulo equality in the first formula (cf. match rule on page 24, section 7.1).

Merge request reports