Reduceを使った定理証明 〜 グレブナー基底を添えて 〜

主専攻実習，定理証明グループ最終発表スライド．Reduceを使った定理証明の解説を，グレブナー基底から，具体的な定理で証明するまで．

Transcript

1. ఆཧূ໌άϧʔϓ 5IFPSFN
   1SPWJOH
   1SBDUJDF !RRIBOO
2. શମઆ໌
3. ϓϩάϥϜͰఆཧূ໌ʁ w ͦΕͬͯͲ͏΍Δͷʁ͓͍͍͠ͷʁ w ԾఆΛஔ͍ͨ࣌ʹɼ݁࿦͕ਖ਼͍͜͠ͱΛࣔͤΕ͹ྑ͍ɽ
4. ४උ
   άϨϒφʔجఈ w ํఔࣜ !" , … , !% → άϨϒφʔجఈ '" , … , '( w ํఔࣜΛղ͖΍͍͢ܗʹม׵ͨ͠΋ͷ w ଟม਺ଟ߲ࣜͷআࢉ ֤εςοϓΛ؆໿ͱΈͳ͢ ʢ.؆໿ SFEVDJUPO PG
   .VMUJQMFTʣ
5. ४උ
   ΠσΞϧ w Մ׵؀RͷΠσΞϧI Rؚ͕ΉIͰҎԼΛຬͨ͢΋ͷ i) %, ' ∈ ) ⟹ % ± ' ∈ ) ii) % ∈ ), , ∈ - ⟹ %, ∈ ) w ྫɿ R = ℤ, I={3
   } 3) 34 ± 35 = 3 4 ± 5 33) 34 5 = 3(45)
6. w ΠσΞϧ ͷഒ਺ Λ 3 ͱॻ͘ɽ 9 ∈ (3) 8 ∉ 3 9 ÷ 3 = 3 ⋯ 0 ͸ͷഒ਺ 8 ÷ 3 = 2 ⋯ 2 ͸ͷഒ਺Ͱ͸ͳ͍ w Ծఆ-. , … , -1 ݁࿦ 2 2 34,…,35 0 ͳΒ 2 ∈ -. , … , -1 ੒Γཱͭอূ͕ͳ͍㱺άϨϒφʔجఈ ℎ. , … , ℎ7 ʹ࡞ Γม͑Δ 2 84,…,89 0 ͳΒ 2 ∈ -. , … , -1 ఆཧΛࣔ͢खॱ
7. ఆཧূ໌ ʰϞϊάϥϑ زԿֶʱ ໼໺݈ଠ࿠ɼਗ਼ٶढ़༤ɽ Qͷఆཧ
8. ʮఆཧ ਖ਼ํܗ"#$%ͷล$%্ͷ఺Λ&ͱ͢Δɽ఺&͔Β "$ʹԼΖͨ͠ਨઢͷ଍Λ1ͱ͠ɼ఺$͔Β"&ʹԼΖͨ͠ ਨઢͷ଍Λ2ͱ͢Δͱɼ఺#
   1
   2͸௚ઢ্ʹ͋Δʯ
9. w ʮఆཧ ਖ਼ํܗ"#$%ͷล$%্ͷ఺Λ&ͱ͢Δɽ఺&͔Β "$ʹԼΖͨ͠ਨઢͷ଍Λ1ͱ͠ɼ఺$͔Β"&ʹԼΖͨ͠ ਨઢͷ଍Λ2ͱ͢Δͱɼ఺#
   1
   2͸௚ઢ্ʹ͋Δʯ w Ծఆ ☐ABCD C−D−E AC ⊥ EP A−C−P AE ⊥ CQ A−E−Q ݁࿦ B−P−Q
10. w Ծఆ ☐ABCD C−D−E AC ⊥ EP A−C−P AE ⊥ CQ A−E−Q ݁࿦ B−P−Q w *+ ࣗ༝ͳ஋ ,+ ଞͷ఺ʹ෇ਵ ܾͯ͠·Δ఺ (0, 0) (*1 , 0) (0, −*1 ) (*1 , −*1 ) (*1 , *2 ) (,3 , ,4 ) (,1 , ,2 )
11. w Ծఆ ☐ABCDʜࣗ໌ C−D−Eʜࣗ໌ AC ⊥ EP ʜ)* A−C−P ʜ
    )+ AE ⊥ CQ ʜ
    )- A−E−Q ʜ
    ). ݁࿦ B−P−Q ʜ/ 3FEVDFϓϩάϥϜ
12. ! "#,…,"& 0 ͱͳͬͨɽ Αͬͯ ! ∈ )* , … , )+ ఆཧ͸ূ໌͞Εͨɽ 3FEVDFϓϩάϥϜ࣮ߦ݁Ռ