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

No alternatives #17

Closed benbrastmckie closed 2 months ago

benbrastmckie commented 3 months ago

One issue seems to persist when a sentence is only verified by the null state. Consider the following constraints:

    # EVAL CONSTRAINTS
    is_world(w),
    # there is a world w

    # A is true in w
    is_part_of(a, w),
    verify(a, A),

    # B is true in w
    is_part_of(b, w),
    verify(b, B),

    # ~(A => B) is true in w
    verify(c, A),
    is_alternative(u, c, w),
    is_part_of(s, u),
    falsify(s, B),

These yield the output:

There is a model of:
A, B, ~(A => B)

States:
  #b00000 = □ (possible)
  #b00010 = b (world)
  #b00100 = c (world)

The evaluation world is b:
  A, B  (true in b)

Propositions:
  |A| = < {□}, ∅ >
  There are no A-alternatives to b

  |B| = < {b}, {c} >
  There are no B-alternatives to b

Since the null state verifies A and is a part of c, it would seem that c should be an A-alternative to b. But this is not what it finds.

benbrastmckie commented 2 months ago

This issue persists in crimson.py.

benbrastmckie commented 2 months ago

That there may fail to be alternatives seems to also explain why the following do not currently work in test_complete.py:

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

This issue seems to be solved.