benbrastmckie / ModelChecker

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

Closure under fusion #16

Closed benbrastmckie closed 4 months ago

benbrastmckie commented 6 months ago

I noticed that verifiers and falsifiers are not closed under fusion despite the closure constraints included in the def proposition. This issue aims to find out why, and how to fix the problem.

benbrastmckie commented 5 months ago

This first issue is solved, however, now I'm wondering if the closure constraint given below is necessary:

    fusion_closure = ForAll([x, y], Exists(z, fusion(x, y) == z))
    solv.add(fusion_closure)
    print(f"Fusion constraint:\n {fusion_closure}\n")

It seems to slightly slow things down, and I'm not sure it is needed. I'll comment out the condition for now from semantics.py. Would be good to confirm whether the constraint can be removed altogether.

benbrastmckie commented 5 months ago

The verifiers for a sentence are not closed under fusion despite the proposition constraints being in place. See the following example in test_complete.py:

input_sentences = ['(A \\boxright B)','\\neg B','\\neg (\\neg B \\boxright \\neg A)']
benbrastmckie commented 4 months ago

This has been resolved.