Simplify conjunctions with weaker subformulas #8

New Issue

patrick · 2018-04-13T01:07:16+02:00

patrick commented

2018-04-13 01:07:16 +02:00

We want to simplify a conjunction F and G where G has a subformula F1 and H such that F1 is weaker than F.

Then, the conjunctive term F1 can be dropped.

For example,

forall V1 (prime(V1) <->
    (V1 in 2..n
        and not exists N1
            (V1 in 1..n and N1 in 2..(V1 - 1) and 0 in (V1 % N1)))).

should become

forall V1 (prime(V1) <->
    (V1 in 2..n
        and not exists N1
            (N1 in 2..(V1 - 1) and 0 in (V1 % N1)))).

We want to simplify a conjunction `F and G` where `G` has a subformula `F1 and H` such that `F1` is weaker than `F`. Then, the conjunctive term `F1` can be dropped. For example, forall V1 (prime(V1) <-> (V1 in 2..n and not exists N1 (V1 in 1..n and N1 in 2..(V1 - 1) and 0 in (V1 % N1)))). should become forall V1 (prime(V1) <-> (V1 in 2..n and not exists N1 (N1 in 2..(V1 - 1) and 0 in (V1 % N1)))).

patrick self-assigned this 2018-04-13 01:07:16 +02:00

patrick added the

enhancement

label 2018-04-13 01:07:16 +02:00

patrick added this to the anthem 0.2.1 milestone 2018-04-23 00:24:44 +02:00

patrick removed this from the anthem 0.2.1 milestone 2019-01-13 16:43:45 +01:00

Sign in to join this conversation.