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

Question

我被困在 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 的错误并不影响公理的真值......

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

Answer 1

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

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

http://www.ffst.hr/~logika/implog/doku.php?id=program:possible_worlds

http://www.personeel.unimaas.nl/roos/EpLogic/start.htm

认识逻辑的实际游戏实现讲座:

http://www.ai.rug.nl/mas/

非常好的博士论文:

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

http://www.harrenstein.nl/Publications.dir/Harrenstein.pdf.gz

关于模态逻辑的讲座(在行动、冲突、游戏中):

http://www.logicinaction.org/

http://www.masfoundations.org/download.html

开放思想的模态逻辑，http://logicandgames.pbworks.com/f/mlbook-almostfinal.pdf (最终版本不是免费的)

关于模态逻辑和一般逻辑的视频讲座:

http://videolectures.net/ssll09_gore_iml/

http://videolectures.net/esslli2011_benthem_logic/

http://videolectures.net/esslli2011_jaspars_logic/

http://www.youtube.com/view_play_list?p=C88812FFE0F526B0