村田 康佑

Articles:  1-1 of 1

  • A Tactic Library for Transforming Inequalities in Coq  [in Japanese]

    村田 康佑 , 江本 健斗

    数学定理やプログラムの性質の形式的証明では,自然数上の不等式についての証明が頻出する.しかし,定理証明支援系Coqでの不等式の形式的証明は,非形式的証明とは異なる記法で記述されるため,数学的な直観がそのまま使えないことも多い.たとえば,非形式的証明では,不等式L ≤ Rを証明するために,しばしばL = M1 ≤ M2 = M3 ≤ ・・・ ≤ Mn = Rのように項を不等号で「鎖状」につなげて示す …

    情報処理学会論文誌プログラミング(PRO) 11(4), 1-12, 2018-12-14

    IPSJ

Page Top