ローワーユニバレンツ

数理論理学の一分野である証明圧縮において、LowerUnivalentsは命題解決証明の圧縮に使用されるアルゴリズムである。LowerUnivalentsはLowerUnitsの一般化されたアルゴリズムであり、ユニットだけでなく、いくつかの追加条件を満たす非ユニット節の部分証明も圧縮することができる。^[1]

参考文献

^ Boudou, J., & Paleo, BW (2013). サブ証明を下げることによる命題解決証明の圧縮。Automated Reasoning with Analytic Tableaux and Related Methods (pp. 59-73)。Springer Berlin Heidelberg。

[1] Boudou, J., & Paleo, BW (2013). サブ証明を下げることによる命題解決証明の圧縮。Automated Reasoning with Analytic Tableaux and Related Methods (pp. 59-73)。Springer Berlin Heidelberg。