含意記号を演算子として持つプログラミング言語
古典命題論理
における
含意
$ a \to b \equiv \lnot a \land b
を演算子として予め持っている
プログラミング言語
及び…
Nix
https://nixos.wiki/wiki/Nix_Expression_Language#Operators
14, IMPL
e1 -> e2
Logical implication (equivalent to
!e1 || e2
).
用例
https://github.com/NixOS/nixpkgs/blob/cbe587c735b734405f56803e267820ee1559e6c1/nixos/modules/services/monitoring/loki.nix#L70-L73
計算したらこれは
XOR
だった．
Alloy
含意演算子
=>
を持つということがリファレンスに書かれている
出典
http://alloytools.org/tutorials/online/sidenote-logic-ops.html
抽象によるソフトウェア設計 Alloyではじめる形式手法(本)
定理証明支援系
あまり正確な記憶がないが，例えば
定理証明支援系
では普通に
=>
か
->
で含意になるケースがある．
Lean 4
はあるのを覚えている．
Coq
はあった気がする．
Isabelle
はどうだったかな