>>333
>充足可能性判定のアルゴリズムは古くて新しい技術である

うん、それ21世紀では、数学というより、コンピュータサイエンス（ソフトウェア科学）（下記）かな（＾＾

（参考）
http://bach.istc.kobe-u.ac.jp/tamura-jp.html
田村 直之 : 神戸大学 情報基盤センター 2017-09-26

http://bach.istc.kobe-u.ac.jp/lecture-jp.html
講義 : 田村 直之 : 神戸大学 情報基盤センター

http://bach.istc.kobe-u.ac.jp/lect/soft/
ソフトウェア科学特論 システム情報学研究科 情報科学専攻 1年生 2017

テキスト
1.命題論理 http://bach.istc.kobe-u.ac.jp/lect/soft/org/proplogic.html
2.命題論理の推論体系 (融合原理) http://bach.istc.kobe-u.ac.jp/lect/soft/org/proplogic-system.html
3.命題論理とSAT http://bach.istc.kobe-u.ac.jp/lect/soft/org/proplogic-sat.html
（SAT (Boolean Satisfiability Testing)は 与えられた命題論理式について， それが充足可能か否かを判定する問題である．）
4.Knuth先生の『TAOCP 7.2.2.2 Satisfiability』を読む http://bach.istc.kobe-u.ac.jp/lect/soft/taocp/index.html

http://bach.istc.kobe-u.ac.jp/lect/soft/org/proplogic.html
ソフトウェア科学特論:
１．命題論理 田村直之 神戸大
(抜粋)
3.5 充足可能性と恒真性
3.5.1 充足可能性の定義

命題論理式 A が， ある真理値割当 v について v(A)=T となる時， v は A を 充足する (satisfies) といい， v|=A で表す．
命題論理式 A について， A を充足する真理値割当が存在する時， A は 充足可能 (satisfiable) であるという．
命題論理式が充足可能でない時， 充足不能 (unsatisfialbe) であるという．

3.5.2 恒真性の定義

命題論理式 A が， 任意の真理値割当により充足される時， A は 恒真 (valid) であると呼ばれ， |=A で表す．
(引用終り)