logic - 克里普克语义 : learning software available?

我被困在 Kripke semantics ，想知道是否有 educational software通过它我可以测试语句的等价性等，因为我开始认为它更容易通过示例学习(即使在抽象变量上)。

我会用

☐A 一定要写 A

♢A 可能是 A

做 ☐true, ☐false, ♢true, ♢false 评估值，如果是这样，来自哪个集合的哪些值或类型的值({true, false} 或可能 {necessary,possably})？ [1]

我想我读了所有 Kripke models使用 duality axiom :

(☐A)->(¬♢¬A)

即如果有必要 paytax那么它不允许不paytax
(无论是否需要纳税...)

即2。如果有必要，到 earnmoney不允许不earnmoney
(再次不管是否真的需要赚钱，逻辑都成立，到目前为止)

因为 A->B 等价于 ¬A<-¬B 让我们测试

¬☐A<-♢¬A

没有必要 upvote如果不允许的话 upvote
这个公理有双重作用:

♢A->¬☐¬A

如果允许 earnmoney那么没有必要不earnmoney
并非所有模式的行为都相同，而且各不相同 Kripke model比另一种更适合建模一种模态:并非所有 Kripke models使用相同的 axioms . (经典量词也是模态吗？如果是这样，Kripke models 是否允许对它们进行建模？)

我将浏览常见公理的列表，并尝试找到使假设看起来违反直觉或不必要的例子......

☐(A->B)->(☐A->☐B):

如果(有必要(赚钱意味着纳税))
那么((挣钱的必要性)意味着(纳税的必要性))

请注意，赚钱并不意味着纳税，蕴涵 A->B 的错误并不影响公理的真值......

呃，在试图理解这一切的过程中表达我的问题需要太长时间......随时编辑

最佳答案

模态逻辑证明者和推理者:

http://www.cs.man.ac.uk/~schmidt/tools/

http://www.cs.man.ac.uk/~sattler/reasoners.html

Java 中的引擎表:

http://www.irisa.fr/prive/fschwarz/lotrecscheme/

https://github.com/gertvv/oops/wiki

http://molle.sourceforge.net/

模态逻辑计算器:

http://staff.science.uva.nl/~jaspars/lvi98/Week3/modal.html