search

benbrastmckie / ModelChecker

A hyperintensional theorem prover for modal, counterfactual conditional, constitutive explanatory, and extensional operators.
https://pypi.org/project/model-checker/
2 stars 0 forks source link

New entailments/relations #12

Closed mbuit82 closed 1 month ago

mbuit82 commented 3 months ago

Hey Ben,

I was trying out the new relations, and I think I have a grasp on how the work loosely. I got a model (as desired) for the second one (top-bottom from those in the TODOs), but I also got a model for the third one (which I don't think should be giving a model). Can you check to make sure those are looking right? Also, I think I found a typo on cf_excl_mid.py—should lines 73, 74, and 78 have t instead of where they currently have s?

benbrastmckie commented 3 months ago

Yes that is a typo, though somehow fixing it does not seem to effect the model that it finds. I'm not totally sure why that is. All the variable binding stuff in Z3 is still a bit of a mystery to me.

Here are some thoughts about the entailment claims:

For A \boxright B, B \boxright C do not entail A \boxright C (in ent_2.py), something does seem to be up. The first part looks right: all the A-alternatives make B true so A => B is true. But it is not the case that all of the B-alternatives make C true, and so B => C should be false. Checking the constraints it looks like there was a missed variable. I noted the change in ent_2.py. But fixing the change still leaves the same problem. You might try swapping all verify to non_null_verify next.

Something similar seemed to be going on for A \boxright B, A \wedge B \boxright C entails A \boxright C (in ent_3.py) since both A and B are true in the A&B-alternative c and yet C is not true there, so (A & B) => C should come out false. Checking the constraints had the same missed variable, but changing it made it yield no models. So this was dead on short of a typo.

But these are looking close, and in a way it is good if we find cases where things don't work so that we can fix them.

mbuit82 commented 3 months ago

with the fixing of the issue in issue #14 , now neither entailment claim produces a model for up to N=5. I did such a small N value because the change from issue #14 seems to make Z3 think a lot longer (longer than a couple mins) once you hit N=6

benbrastmckie commented 3 months ago

I thought maybe the new trouble was due to removing 'simplify' from the 'bit_part' def, but I added it back and still trouble.

benbrastmckie commented 3 months ago

I think the issue might be all_bits. I added a print clause to print.py to indicate what these are. It seems that in general there are far too few, and this likely explains why it isn't populating any fusions of verifiers, alt_worlds, etc.

This may also also fix #16 and #14.

benbrastmckie commented 1 month ago

This has been resolved.