Mastodon

ソフトウェア・ライセンスの命題論理

ソフトウェア・ライセンスのプランを変更する際に命題論理を用いて,形式的に機能制限の設計を行うことができる.

たとえば,次のようにプランが再設計されたものとする.

$$
\begin{align}
p &\implies v \\
q &\implies v \lor w
\end{align}
$$

ここに,$${p}$$や$${v}$$などはプランの種名辞である.上の式は,プラン$${p}$$が$${v}$$に変更され,またプラン$${q}$$が$${v}$$と$${w}$$に分割されたことを表している.含意記号を用い,プランの再設計を写像として表現している.

プランの変更前は,プラン$${p}$$か$${q}$$に加入していれば機能$${\psi}$$が利用可能であったとしよう.これは,論理式として次のように表現できる.

$$
\psi \implies p \lor q
$$

ここに,$${ p \lor q \implies \psi}$$ではないことに注意しよう.この命題論理式が真であれば,$${p \lor q}$$が偽,すなわちプラン$${p}$$と$${q}$$のどちらにも加入していないときにも機能$${\psi}$$が利用可能となることがあってしまう.

我々がいますべきことは,$${v}$$と$${w}$$で機能$${\psi}$$が利用可能となる条件を記述することである.
以上の論理式より次が導ける.

$$
\begin{align}
\psi
&\implies p \lor q \\
&\implies v \lor (v \lor w) \\
&\implies v \lor w
\end{align}
$$

したがって,機能$${\psi}$$を利用するために加入する必要のあるプランは$${v}$$または$${w}$$であることがわかる.

このように,プランと利用可能な機能の制限を設計する際に命題論理を用いることで,形式的に設計の妥当性を確認することができる.