Open biaktfn opened 5 months ago
For example, we can input:
1: (^want,{SELF},<a --> b>). %1.00;0.90%
And it will create a goal:
2: \b>! %1.000;0.900%
Then we can also ask:
3: \<a --> b>?
It will create a judgement:
4: <(*, {SELF}, \b>)-->^wonder>. :|: %1.000;0.900%
The inference rule can apply on 1 and 4, so there will be:
<^wonder-->^want>. %1.000;0.299% <^want-->^wonder>. %1.000;0.299%
which are obviously should not be derived.
Describe the bug
For example, we can input:
And it will create a goal:
Then we can also ask:
It will create a judgement:
The inference rule can apply on 1 and 4, so there will be:
which are obviously should not be derived.