2013-02-24から1日間の記事一覧
古典論理での〜の導入(INTRO)と消去(ELIM)の推論には,以下の4通りがあります. 〜A|- |-〜A −−−− −−−− |-A A|- (UNDISCH o NOT_ELIM) |-A A|- −−−− −−−− 〜A|- |-〜A NEG_DISCH,(NOT_INTRO o DISCH) # ARITH_RULE `~(n<0)`;; val it : thm = |…
古典論理での〜の導入(INTRO)と消去(ELIM)の推論には,以下の4通りがあります. 〜A|- |-〜A −−−− −−−− |-A A|- (UNDISCH o NOT_ELIM) |-A A|- −−−− −−−− 〜A|- |-〜A NEG_DISCH,(NOT_INTRO o DISCH) # ARITH_RULE `~(n<0)`;; val it : thm = |…