2011-11-18から1日間の記事一覧
今回は,特称量化にも対応した一般の半代数系の prover についてです.■ まず,:num,:intにおける線形系のそれは #use "Examples/cooper.ml";; とロードして使う,Cooperのアルゴリズムに基づく関数,COOPER_RULE,INT_COOPERです. # ARITH_RULE `?x. 0=x`…
今回は,特称量化にも対応した一般の半代数系の prover についてです.■ まず,:num,:intにおける線形系のそれは #use "Examples/cooper.ml";; とロードして使う,Cooperのアルゴリズムに基づく関数,COOPER_RULE,INT_COOPERです. # ARITH_RULE `?x. 0=x`…