Skip to content
Permalink
Branch: master
Commits on Feb 5, 2020
  1. Merge branch 'tseitinQ'

    wo committed Feb 5, 2020
  2. tidy up

    wo committed Feb 5, 2020
Commits on Feb 4, 2020
  1. tidy up

    wo committed Feb 4, 2020
  2. modelfinder bugfixes

    wo committed Feb 4, 2020
    Signed-off-by: wo <wo@umsu.de>
  3. modelfinder bugfixes

    wo committed Jan 16, 2020
Commits on Jan 15, 2020
  1. ignore

    wo committed Jan 15, 2020
  2. ignore

    wo committed Jan 15, 2020
Commits on Jan 14, 2020
Commits on Jan 13, 2020
  1. better status

    wo committed Jan 13, 2020
Commits on Jan 11, 2020
Commits on Jan 10, 2020
  1. use tseitin transformation in modelfinder

    wo committed Jan 10, 2020
    The naive CNF algorithm produces 16384 clauses for ((∃x∀y(Px↔Py)↔(∃zQz↔∀wQw))↔(∃x2∀x3(Qx2↔Qx3)↔(∃x4Px4↔∀x5Px5))). I now use tseitin transformations.
Commits on Dec 3, 2019
  1. improve processing of alternative trees in backtracking

    wo committed Dec 3, 2019
    When reaching the depthLimit, I used to discard the current tree and switch to
    one of its alternatives; when there were no alternatives left, I increased the
    depthLimit and kept working with the last tree.
    
    This is not ideal because the last tree in the list of alternatives is often not
    the simplest, and we effectively never reconsider the earlier
    alternatives. Restarting the tree construction from scratch whenever the
    depthlimit is reached fixes this, but it creates a lot of redundancy.
    
    This patch instead keeps the alternatives in memory even when depthlimit is
    reached. When the limit is increased, we simply go back to the first alternative
    and expand it some more.
Commits on Oct 29, 2019
  1. update documentation

    wo committed Oct 29, 2019
  2. bugfix: don't get stuck in modalGamma loops when new node is already …

    wo committed Oct 29, 2019
    …on branch
    
    In the S4 tree for (A ∧ ¬□A)→□¬□A, (¬A ∧ ◇A)→□◇A |= ◇□A→□◇A the tree construction got stuck in a loop at step 57. Here (or in 60 etc.), it should try expanding the modalGamma formula with w2 instead of w1, but it kept trying w1 because the result of that modalGamma application is already on the branch, so it couldn't find it when looking if an instance term has already been used.
  3. add test

    wo committed Oct 29, 2019
  4. improve modelfinder

    wo committed Oct 29, 2019
Commits on Oct 21, 2019
  1. tidy up

    wo committed Oct 21, 2019
Commits on Oct 20, 2019
Commits on Oct 13, 2019
  1. fix readme

    wo committed Oct 13, 2019
  2. mark beta origins of pruned branches as unused

    wo committed Oct 13, 2019
    In the S5 proof for (□p↔◇q)→◇(p↔q) this caused a redundant node 21 (in step 31).
Commits on Oct 12, 2019
  1. improve accessibility rules

    wo committed Oct 12, 2019
  2. improve accessibility rules

    wo committed Oct 12, 2019
Commits on Sep 13, 2019
Commits on Sep 12, 2019
Commits on Sep 4, 2019
Older
You can’t perform that action at this time.