2020-03-27 16:49:59 (GMT)
The Boolean PAAR paper says that BoolSimp can be applied with any substitution. That doesn't sound right. Then I could apply x ↦ y to x ⋁¬ y and then simplify to ⊤.
2020-03-27 17:0:39 (GMT)
Substitution is applied to the rules
2020-03-27 17:1:35 (GMT)
and then some instance of the left hand side appears in the clause
2020-03-27 17:2:2 (GMT)
For the rule to be applicable y \/ ~y must appear as a subterm
2020-03-27 17:3:48 (GMT)
Oh, the p in the rules is a variable?
2020-03-27 17:10:13 (GMT)
yes
2020-03-27 17:10:38 (GMT)
this is the notation we set in Section 2
2020-03-27 17:11:24 (GMT)
ok
2020-03-27 17:11:36 (GMT)
haven't read section 2, my fault :D
2020-03-27 17:12:10 (GMT)
no worries
any substitution might be a bit confusing
and Section 2 was shamelessly stolen from you