形式体系に基づく実証明の分析

全文

(1)形式体系に基づく実証明の分析加藤あや美南山大学大学院数理情報研究科佐々木克巳南山大学情報理工学部

(2) . 概要本研究は、シークエント体系に基づいて、集合の分野で扱われている定理の証明を分析する。本研究で扱う定理は、ド・モルガン律と分配律である。具体的には、冊の文献から証明を抽出し、それらを体系に基づいた方法で表現し、分類・整理する。また、この分類毎に、多く用いられた推論規則を用いた証明の形を作成する。. はじめに本研究は、集合の分野で扱われている定理の証明を分析する。本研究で扱う定理は、ド・モルガン律と分配律、すなわち、つの集合に対する次のつの性質である。性質性質性質性質 . . . . これらのつの性質に対し、次の手順でその証明を分析する。 . 各性質に対して、文献から証明を抽出する。. !. 手順で抽出した証明をシークエントの変化で表現する。この表現を、実際の証明図と名付ける。. . 手順 ! の証明図に、推論規則を補って証明図を作成する。この証明図を、省略なしの証明図と名付ける。. . 手順の証明図を、その形から分類する。. ". 各分類に対して、多く用いられている推論規則の組み合わせを調べる。. . 手順 " の結果から、適切な証明図を作成する。. #. 各性質に対し、方法の右左と左右を比較する。. 手順において、性質の証明は文献 "$!# から、性質 ! の証明は文献 !$ から、性質の証明は文献 $! から、性質の証明は文献 !$" から抽出した。これらの証明は、次のいずれかの方法で示されていた。方法. 左辺. 右辺と. 右辺. 左辺を示す方法 .

(3) 方法 . 左辺右辺を示す方法. 以下、方法の左辺右辺右辺左辺をそれぞれ左右右左と略記する。以下の、! 節では本研究で用いる体系について述べる。節では、ド・モルガン律に対して手順 !∼ を行った結果について述べる。節では、ド・モルガン律に対して手順 "∼ を行った結果について述べる。 " 節では、分配律に対して手順 !∼ を行った結果について述べる。節では、分配律に対して手順 "∼ を行った結果について述べる。 # 節では、手順 # について述べる。. . 体系この節では、本研究で用いる体系について述べる。論理式は次の言語を用いて、普通の方法で定義する。 . 対象変数 . !. 述語記号. . 集合集合集合. 論理記号. に対して、変数の述語記号 %. &. に対して、$ 変数の述語記号 % & に対して、$ 変数の述語記号 % &. かつまたはならばでないすべて. 論理式を表すのに、 ½ ¾ …などの記号を、論理式の有限集合を表すのに '( を用いる。また、論理式をと略記する。論理式の解釈は、述語記号をそのまま集合の文と解釈し、各論理記号をそのまま日本語に反映させて解釈して定まるものとする。本研究では、論理式とからその解釈で定まる文を同一視して、その文もで表すことにする。体系の定義は、文献 # に従う。ここでは、その概観を述べる。まず、式について述べる。表現 '.

(4) . を式という。' をこの式の左辺、を右辺という。左辺に % &%&% & が出現するときは、適宜省略する。例えば、. ½ ¾ . を. '.

(5) . ½ ¾ '

(6) . のように省略する。次に、推論規則について述べる。式 ½ … に対し、図式. ½. ・・・. . を推論規則という。をこの推論規則の下式、各をこの推論規則の上式という。最後に、証明図について述べる。証明図は、公理

(7) と推論規則から普通の方法で定義する。証明図の一番下の式を終式、一番上の式を始式という。なお、証明図は終式から上に向かって作成することが多いので、ある推論規則を優先するとは、この推論規則を証明図の下側で適用することとする。 !.

(8) 本研究では、実際の証明に近い証明図を作成したいので、文献 # の推論規則

(9) をより具体的に定義し、さらにいくつかの推論規則を文献 # の推論規則に追加する。以下、集合を表す記号として、などを用いる。文献 # では、文 ½ が文 ¾ により定義されているとき、. ¾ '

(10) '

(11) ¾ ½ '

(12) '

(13) ½ の ! つの推論規則

(14) に導入した。 ½ ¾ の具体的な関係は表に定める。表には、各 ½ ¾ に対応する推論規則の名前も記しておく。表 . ½. 名前.

(15)

(16).

(17). ¾. .

(18) 差

(19) 補

(20) ※

(21) ) ※. が集合を表す変数のときは、 . と. . を同一視してこれを推論規則としない。. 文 ½ と文 ¾ に. ½ ¾ がよく用いられている性質である。という関係があるときも、の形の推論規則を推論規則に追加する。 ½ ¾ の具体的な関係は表 ! のとおりであり、そこでは各 ½ ¾ に対応する推論規則の名前も記しておく。表 ! 追加すべき推論規則. 名前. ! !. の律. ½ ¾ . また、論理式 * に現れる論理式 ½ のいくつかを論理式 ¾ で置き換えた論理式をしたとき、表表 ! の ½ ¾ の組に対して、. ¾ ½. と. ¾ ½ '

(22) '

(23) ¾ ½ '

(24) '

(25) を追加する。この推論規則の名前は、 ½ ¾ に対する表の規則の名前に+をつけたものとする。. さらに、次のつの推論規則も追加すべき推論規則に追加する。 .

(26) ' '. '. '

(27)

(28)

(29) . '. '.

(30)

(31) '

(32) .

(33) '

(34)

(35) " '

(36) . '.

(37).

(38)

(39) !.

(40) '

(41)

(42) '

(43) .

(44)

(45)

(46) . '

(47) '

(48) '

(49) '

(50) '

(51) . '

(52) '

(53) .

(54) . !. 選言三段論法. 表 ! の !!の律と、それに+をつけた !!の律、および、最後に追加したつの推論規則

(55)

(56) !

(57)

(58)

(59) "

(60) ! 選言三段論法を追加すべき推論規則と呼ぶ。. . ド・モルガン律の証明の分類. この節では、ド・モルガン律に対して手順 !∼ を行った結果について述べる。手順における文献は "$!# である。. . 実際の証明図. まず、手順 ! で作成した実際の証明図について述べる。作成方法は、次のとおりである。. . 上式が下式よりも簡単になる。. . 左辺の推論規則を優先する。. 本研究では、冊の文献から抽出した証明文に対し、実際の証明図を作成した。以下に、方法で証明している文献から ! つを抽出し、その右左の実際の証明図を示す。左の証明図が、文献 " 右左であり、右の証明図が、文献右左である。.

(61)

(62)

(63)

(64)

(65) .

(66)

(67)

(68)

(69) . なお、一般にはつの証明に対して、複数の「実際の証明図」をかくことができる。文献 " の右左の証明から、別の方法で作成した「実際の証明図」を以下に示す。 .

(70)

(71)

(72)

(73)

(74)

(75) 省略なしの証明図次に、手順で作成した省略なしの証明図について述べる。省略なしの証明図とは、次のように作成された証明図である。. . . 実際の証明図における推論規則のうち、推論規則以外のものを、次のいずれかの推論規則の組み合わせで表現する。・

(76) $ 個か ! 個の

(77) の組み合わせ・

(78)

(79) $ 個か個の

(80) の組み合わせ・$ 個以上の

(81) $ 個以上の

(82) $ 個以上の

(83) $ 個か個のそれ以外の規則の組み合わせ方法を使用した証明図の推論規則を補う際、すべての上式が公理になる推論規則は省略する。. . 方法 ! を使用した証明図は、始式を省略する。. . 推論規則を補う優先順位は、以下の小さい番号のものを図の下側に補う順位とする。 !. . . .

(84)

(85) 追加すべき推論規則の律は方法 ! の場合のみ使用し、! つ以上が適用できるときは全体が短くなるものを優先する。.

(86)

(87) . 上の ! のそれぞれにおいて、右辺あるいはの右を主論理式とする推論規則は、左辺あるいはの左を主論理式とする推論規則を適用できないときのみに適用する。. 証明の分類. 最後に手順の結果、すなわち、手順の結果から証明を分類した結果について述べる。! 節の方法で作成した省略なしの証明図が同じ証明、または、その省略なしの証明図の推論規則の順番のみ異なる証明は、同じ分類に属すとした。性質について述べる。性質の分類は、" 種類あった。. ".

(88) 次の省略なしの証明図に対応する証明を、分類とおく。文献は、! ! である。.

(89)

(90)

(91)

(92) 差

(93)

(94)

(95)

(96)

(97)

(98)

(99)

(100)

(101) 差

(102)

(103)

(104)

(105)

(106)

(107)

(108)

(109)

(110)

(111)

(112)

(113)

(114)

(115) 差

(116)

(117) 差

(118)

(119)

(120)

(121)

(122)

(123)

(124)

(125)

(126)

(127) 次の「と」または「と」の省略なしの証明図に対応する証明を、分類 ! とおく。文献はの形が " 、の形がである。" ページでは、文献 " の、別の方法で作成した証明も示した。その証明から省略なしの証明図を作るととなる。その意味で、とは同じ分類に属すと考えた。左の証明図が、であり、右の証明図が、である。.

(128)

(129)

(130)

(131)

(132)

(133) 補

(134)

(135) 補

(136)

(137)

(138)

(139)

(140)

(141)

(142)

(143)

(144)

(145) .

(146) 補

(147)

(148)

(149)

(150)

(151) .

(152)

(153)

(154)

(155) 補

(156)

(157)

(158)

(159)

(160)

(161)

(162)

(163) . の部分は、. と同じである. .

(164) .

(165) 補

(166).

(167)

(168)

(169)

(170) 補

(171)

(172)

(173) . 次の省略なしの証明図に対応する証明を、分類とおく。文献は、$# である。補

(174)

(175)

(176)

(177)

(178) .

(179)

(180)

(181)

(182) 補

(183)

(184)

(185)

(186)

(187) 次の省略なしの証明図に対応する証明を、分類とおく。文献は、である。は、全体集. 合である。の部分は、分類と同じである. の律

(188)

(189)

(190)

(191)

(192) .

(193)

(194)

(195)

(196) 補

(197) . 補

(198) . . 次の省略なしの証明図に対応する証明を、分類 " とおく。文献は、である。. の律

(199) 差

(200)

(201)

(202)

(203)

(204) .

(205)

(206)

(207)

(208) 差

(209)

(210)

(211)

(212)

(213) 結果として " つの分類は、表に示す性質をもつ。この表より、" つの分類が証明すべき形およびその方法による分類と一致しているということが分かる。 #.

(214) 性質 ! について述べる。性質 ! の分類は、種類あった。次の省略なしの証明図に対応する証明を、分類 ! とおく。文献は、! である。.

(215)

(216) .

(217)

(218)

(219) 差

(220) !

(221)

(222)

(223)

(224)

(225)

(226) 差

(227)

(228)

(229)

(230)

(231)

(232)

(233)

(234) !

(235)

(236)

(237)

(238)

(239) 差

(240)

(241)

(242) 差

(243)

(244)

(245)

(246)

(247)

(248)

(249)

(250)

(251)

(252) 次の省略なしの証明図に対応する証明を、分類 !! とおく。文献は、である。.

(253) 差

(254)

(255) .

(256)

(257) !

(258)

(259)

(260)

(261)

(262)

(263) 差

(264)

(265)

(266)

(267) . .

(268) 次の省略なしの証明図に対応する証明を、分類 ! とおく。文献は、$ である。補

(269)

(270)

(271)

(272) !

(273)

(274)

(275)

(276)

(277) 補

(278)

(279)

(280)

(281)

(282) 結果としてつの分類は、表に示す性質をもつ。この表より、つの分類が証明すべき形およびその方法による分類と一致しているということが分かる。. 分類. . 分類分類 ! 分類分類 . . . 分類 ". 分類分類 ! 分類 !! 分類 !. . . . . . 表性質の分類証明方法. . を方法で示す. を方法 ! で示し、 . . を用いるを用いる. を方法 ! で示す. 表性質 ! の分類証明方法. . . . !!. を方法で示す. を方法 ! で示し、 . . 文献. . を方法で示すを方法 ! で示す. を方法 ! で示す. " $# . 文献 ! $. ド・モルガン律の証明の分析この節では、ド・モルガン律に対して手順 "∼ を行った結果について述べる。. . 推論規則の組み合わせ. まず、手順 " の結果について述べる。この手順における推論規則の組み合わせとは、「省略なしの証明図に現れる推論規則」の組み合わせで、もとになる実際の証明図に用いられているものである。文献ごとの推論規則の組み合わせを、性質については表 " に、性質 ! については表にまとめた。さらに、複数の文献の証明で構成される各分類 !! に対して、使われていた推論規則の組み合わせを表 # にまとめた。方法で証明していた文献は、証明の向きを「左右」と .

(283) 「右左」で示した。ただし、その推論規則の組み合わせを左右と右左で行っていた場合は「両方」と表記した。. 文献. 表 " 性質の推論規則の組み合わせ推論規則の組み合わせ証明の向き. # ! ! " $ . . 文献 !. $ . .

(284)

(285)

(286)

(287)

(288)

(289).

(290)

(291)

(292)

(293)

(294).

(295)

(296)

(297) 補

(298)

(299)

(300)

(301)

(302)

(303) 補

(304)

(305)

(306)

(307).

(308)

(309)

(310) 補

(311)

(312) 補

(313)

(314)

(315) . 両方両方両方両方. 左右右左左右両方. 表性質 ! の推論規則の組み合わせ推論規則の組み合わせ証明の向き.

(316)

(317)

(318).

(319)

(320) ! 差

(321)

(322)

(323) !

(324)

(325) 差

(326)

(327)

(328) !

(329) 補

(330)

(331)

(332)

(333)

(334) ! 補

(335)

(336) . 両方左右右左右左. 適切な証明図. 次に、手順の結果について述べる。ここで述べる適切な証明図とは、多くの文献で用いられている推論規則の組み合わせで構成された証明図のことである。具体的には、複数の文献の証明で構成される分類を対象として、次の $.

(337) 分類 !. . !. 表 # 分類ごとの推論規則の組み合わせ推論規則の組み合わせ証明の向き文献の数使ったいた文献,全文献.

(338)

(339)

(340).

(341)

(342)

(343)

(344)

(345).

(346)

(347)

(348).

(349)

(350)

(351) 補

(352)

(353)

(354)

(355) 補

(356)

(357)

(358)

(359) 補

(360)

(361)

(362) 補

(363)

(364) 補

(365)

(366)

(367)

(368) ! 補

(369)

(370) . 両方両方. 左右右左右左両方左右. , , !,! ,! ,! !,! ,! , , , , !,! ,! ,! ,!. ように適切な証明図を作成した。 . 「省略なしの証明図に現れる推論規則」の組み合わせのうち、実際の証明図に用いられているものを抽出する。. ! . で抽出した組み合わせのうち、全体の半数以上で使われていたものを抽出する。. ! で抽出した組み合わせの中で、共通の推論規則が含まれている ! つ以上の組み合わせがあっ. た場合、それらの組み合わせを合併した組み合わせを採用する。 . で採用した組み合わせをつなげてできる証明図を、適切な証明図とする。. 本研究が対象とした証明の範囲では、この方法で適切な証明図が一意に定まる。分類ごとの適切な証明図は、次のとおりである。ここでは、推論規則の組合せの名前は、組み合わされた推論規則を並べたものとした。さらに、それらが、

(371) の左辺と右辺のどちらについて行っているものかを分かりやすくするために、各推論規則の名前に

(372) をつけた。分類 .

(373) 差

(374)

(375)

(376)

(377)

(378)

(379)

(380)

(381)

(382)

(383)

(384) 差

(385)

(386)

(387)

(388)

(389)

(390)

(391) . .

(392)

(393)

(394)

(395)

(396)

(397)

(398)

(399) 差

(400)

(401) 差

(402)

(403)

(404)

(405)

(406)

(407)

(408)

(409)

(410)

(411) . 分類 !.

(412)

(413)

(414) 補

(415)

(416)

(417)

(418)

(419)

(420)

(421)

(422) 補

(423)

(424)

(425)

(426)

(427)

(428)

(429)

(430)

(431)

(432)

(433)

(434)

(435) .

(436)

(437)

(438) 補

(439)

(440)

(441)

(442) 補

(443)

(444)

(445)

(446)

(447)

(448) . 分類補

(449)

(450)

(451)

(452)

(453)

(454)

(455) 補

(456)

(457)

(458)

(459) 分類 ! 補

(460)

(461)

(462)

(463) .

(464)

(465)

(466) !

(467) 補

(468)

(469) . . 分配律の証明の分類. この節では、分配律に対して手順 !∼ を行った結果について述べる。手順における文献はである。ただし、文献の証明は、もとの証明文の意図を正しく反映しているか曖昧なので対象から外す。実際の証明図の作成方法手順 ! と省略なしの証明図の作成方法手順）は節と同様である。ただし、後者は、次の # つの式の上には推論規則を補わない。 # つのうち、最初の ! つを、それぞれ式式 ! とおく。. !.

(470)

(471)

(472)

(473)

(474)

(475)

(476)

(477) . . 手順の結果、すなわち、手順の結果から証明を分類した結果について述べる。方法の証明は、右左の証明と左右の証明を独立に分類する。性質の分類方法は、節と同じである。性質については、性質と同様の分類の仕方に加えて、分岐後の枝の部分のみが違う証明図も同じ分類に属すとした。性質について述べる。性質の分類は、方法左右が ! 種類、右左が種類、方法 ! が種類であった。次の「または」の省略なしの証明図に対応する証明を、分類 ¼ とおく。文献はの形が $ 、の形が $ である。. . .

(478)

(479)

(480) .

(481)

(482) .

(483)

(484)

(485)

(486)

(487)

(488)

(489) の部分は、. と同じである.

(490)

(491)

(492) .

(493)

(494) . なお、文献 $ の証明の作り方を変えると、省略なしの証明図がになるようにできる。次の「または」の省略なしの証明図に対応する証明を、分類 ! とおく。証明の向きは左右である。文献はの形が ! 、の形が ! である。. .

(495) . .

(496)

(497)

(498)

(499)

(500)

(501) .

(502)

(503)

(504)

(505)

(506)

(507)

(508)

(509)

(510)

(511) の部分は、. と同じである.

(512)

(513)

(514)

(515)

(516)

(517) . なお、文献 ! の実際の証明図の作り方を変えると、省略なしの証明図がになるようにできる。次の「またはまたは」の省略なしの証明図に対応する証明を、分類とおく。証明の向きは左右である。文献はの形が、の形が、の形がである。. .

(518)

(519)

(520)

(521)

(522)

(523)

(524)

(525)

(526)

(527)

(528)

(529)

(530)

(531)

(532)

(533)

(534)

(535)

(536)

(537)

(538)

(539)

(540)

(541)

(542)

(543) . の部分は、. と同様である.

(544)

(545)

(546) 左と同様

(547)

(548)

(549)

(550) . .

(551) . の部分は、. と同様である

(552)

(553)

(554)

(555)

(556)

(557)

(558)

(559)

(560)

(561)

(562)

(563) . なお、文献の省略なしの証明図の作り方を変えると、その省略なしの証明図がになるようにできる。また、文献の省略なしの証明図の作り方を変えると、その省略なしの証明図がになるようにできる。次の「または」の省略なしの証明図に対応する証明を、分類 !¼ とおく。証明の向きは右左である。文献はの形が、の形が ! である。. . .

(564)

(565)

(566)

(567)

(568)

(569)

(570)

(571)

(572)

(573)

(574)

(575)

(576)

(577)

(578)

(579) の部分は、. と同じである

(580)

(581)

(582)

(583)

(584)

(585) . 文献の証明の作り方を変えると、省略なしの証明図がになるようにできる。その意味で、これらの ! つは同じ分類にできると考えた。次の省略なしの証明図に対応する証明を、分類 ¼ とおく。証明の向きは右左であり、文献はである。.

(586)

(587)

(588)

(589)

(590)

(591)

(592)

(593) 左と同様

(594)

(595)

(596)

(597)

(598)

(599)

(600)

(601)

(602)

(603)

(604)

(605) ".

(606) 次の省略なしの証明図に対応する証明を、分類 ¼ とおく。証明の向きは右左であり、文献はである。.

(607)

(608)

(609).

(610)

(611)

(612) .

(613)

(614) ". 結果としてつの分類は、表に示す性質をもつ。表性質の分類分類. 証明の方法. 文献. 分類 . を用いる. $. 分類 .

(615) を用いる. . 分類 ¼. を用いる. $. 左右分類 ! 右左. ¼. 分類 !. ¼. 分類 . ¼. 分類 . を用いる . を用いる.

(616) を用いる.

(617)

(618) " を用いる. !!. ! . 性質について述べる。性質の分類は、方法左右が種類、右左が種類、方法 ! が種類であった。次の省略なしの証明図に対応する証明を、分類 ¼ とおく。文献は、$ である。. !

(619)

(620)

(621)

(622)

(623)

(624)

(625)

(626)

(627)

(628)

(629)

(630) 次の「または」の省略なしの証明図に対応する証明を、分類 ! とおく。証明の向きは左右である。文献は ½ は左の形の形が !"" 、 ½ は右の形の形が、の形がである。. .

(631) .

(632)

(633)

(634)

(635)

(636) ½

(637)

(638)

(639)

(640)

(641)

(642)

(643)

(644)

(645)

(646)

(647)

(648) .

(649)

(650)

(651)

(652)

(653) . ただし、½ は以下のいずれかの形である。.

(654)

(655)

(656)

(657)

(658)

(659) . .

(660)

(661) . . 式. の部分は、と同じであり、½ は上の右の形である. ½.

(662)

(663)

(664)

(665)

(666) 左と同様

(667)

(668)

(669)

(670)

(671) . 次の省略なしの証明図に対応する証明を、分類とおく。証明の向きは左右であり、文献はである。.

(672)

(673)

(674) !

(675)

(676)

(677) .

(678) !

(679) . 次の省略なしの証明図に対応する証明を、分類とおく。証明の向きは左右であり、文献はである。.

(680) !

(681)

(682)

(683)

(684)

(685)

(686)

(687)

(688)

(689)

(690)

(691)

(692)

(693)

(694)

(695) #.

(696) 次の「または」の省略なしの証明図に対応する証明を、分類 !¼ とおく。証明の向きは右左である。文献は ½ は上の形の形が、 ½ は下の形の形が " 、の形がである。 ½ は左の形の証明図の「のとき」の始式が異なっている証明図がである。 ½ は左の形の証明図の「のとき」の証明について、さらに場合分けをしている証明図がである。. .

(697)

(698)

(699) ½

(700)

(701)

(702)

(703)

(704)

(705)

(706)

(707)

(708) . ただし、½ は以下のいずれかの形である。.

(709)

(710)

(711)

(712)

(713)

(714)

(715)

(716) 選言三段論法.

(717)

(718)

(719)

(720)

(721)


(723)

(724)

(725)

(726)

(727)

(728) . . の部分は、と同じである.

(729)


(731)

(732)

(733)

(734)

(735) 式 !

(736)

(737)

(738)

(739)

(740) . 次の「または」省略なしの証明図に対応する証明を、分類 ¼ とおく。証明の向きは右左である。文献はの形が ! 、の形が " である。. .

(741) . .

(742)

(743) 選言三段論法 .

(744)

(745) !

(746)

(747)

(748)

(749)

(750)

(751)

(752)

(753)

(754)

(755)

(756)

(757)

(758) . の部分は、と同じである.

(759)


(761)

(762)

(763)

(764)

(765) ! . 次の省略なしの証明図に対応する証明を、分類 ¼ とおく。証明の向きは右左であり、文献はである。.

(766)

(767)

(768)

(769)

(770)

(771) !

(772)

(773)

(774)

(775)

(776)

(777)

(778)

(779)

(780)

(781)

(782)

(783)

(784)

(785)

(786)

(787)

(788) . 次の省略なしの証明図に対応する証明を、分類 "¼ とおく。証明の向きは右左であり、文献はである。. !

(789)

(790)

(791)

(792)

(793)

(794)

(795)

(796)

(797)

(798)

(799)

(800)

(801)

(802)

(803) .

(804) 結果としてつの分類は、表に示す性質をもつ。表性質の分類分類. 証明方法. 左右. を用いる

(805) を用いる. 分類分類 ! 分類 .

(806) !

(807) を用いる ! を用いる. 分類 ¼. を用いる. 分類右左. ¼. 分類 !. ¼. 分類 . ¼. 分類 . ¼. 分類 ". 選言三段論法を用いる ! 選言三段論法を用いる

(808) ! を用いる ! を用いる. 文献 $ !"" $ " !" . 分配律の証明の分析この節では、分配律に対して手順 "∼ を行った結果について述べる。. . 推論規則の組み合わせ. まず、手順 " の結果について述べる。この手順における推論規則の組み合わせとは、「省略なしの証明図に現れる推論規則」の組み合わせで、もとになる実際の証明図に用いられているものである。文献ごとのの推論規則の組み合わせを、性質については表 $ に、性質については表にまとめた。さらに、複数の文献の証明で構成される各分類 !¼ !¼ !¼ !¼ ¼ "¼ に対して、使われていた推論規則の組み合わせを表 ! にまとめた。ただし、分類 ! は、 ½ は左の形の形のみを対象とし、分類 !¼ は ½ は下の形のみを対象とする。これら表における「証明の向き」の意味は、節と同じである。. !$.

(809) 表性質の推論規則の組み合わせ文献推論規則の組み合わせ証明の向き . 表 $ 性質の推論規則の組み合わせ文献推論規則の組み合わせ証明の向き ! $ . . !. . .

(810)

(811)

(812).

(813)

(814)

(815)