This project is maintained by AkihisaYamada

The 15th Theorem Proving and Provers meeting (TPP 2019)

TPP (Theorem Proving and Provers) ミーティングは, 2005年から年に1回開催され, 定理証明系を作っている人から使う側の人まで幅広い人たちが集まり, 様々な側面からの話をしてアイディアの交換をしてきたものです.

ミーティング期間中の討論を大切にしたいと考えていますので, 出来上がった仕事の講演だけでなく,進行中の仕事,未完成の仕事についての講演も歓迎します. 参加者には可能な限りご講演いただくことを期待しています.

TPP is a series of annual meetings for developers as well as users of theorem provers. Discussions from various aspects and exchanges of ideas have taken place in the past meetings since 2005.

We regard the discussions during the meeting to be most important. As such, not only the talks about completed work, but those about ongoing work and half-baked work are also welcome. We hope all participants would consider giving a talk.

開催日程 / Date

2019年11月18日(月), 19日(火) / Mon. 18th to Tue. 19th, November.

会場 / Venue

国立情報学研究所(学術総合センター)19階 1901,1902,1903会議室 / National Institute of Informatics (National Center of Sciences) 19th floor, Rooms 1901, 1902, 1903

住所 / Address

〒101-8430 東京都千代田区一ツ橋2-1-2 / 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430 アクセス / Access

懇親会 / Dinner Party

日時: 11/18 18:30~ / Time: 18th Mon. 18:30~

会場 / Place: まごころ居酒屋 芝浦 神保町店 (On Google Map)

幹事 / Organizer

山田晃久 (国立情報学研究所, ERATO蓮尾メタ数理システムデザインプロジェクト) / Akihisa YAMADA (ERATO HASUO Metamathematics for Systems Design Project, NII)

Email: akihisayamada<at>

参加申し込み / Registration

11/13(水)までに / Please register by 13th November from

こちらから / here

プログラム / Technical Program

Nov. 18

Nov. 19


計算可能性を形式化するための土台をみんなで考えてみるというのはいかがでしょうか. ただ教科書的な題材では面白くないかもしれませんので,少しひねくれたものになっています. 解答はオーガナイザーまでお送りください.部分解・アップデートも歓迎します. / How about collectively think of a foundation for formalizing computability? As the textbook theme might be boring to you, below offers a slightly screwed up setting. Solutions should be send to the organizer. Partial solutions and updates are welcome.

  1. Cyclicテープ上で動くチューリングマシンの概念を形式的に定義してください. Cyclicテープとは固定長のテープで,両端がつながったものです. ベースとなるチューリングマシンの定義は問いません./ Please formally define a notion of Turing machines that manipulate cyclic tapes. A cyclic tape is a fixed-length tape whose both ends are connected to each other. You can base on any paper definition of Turing machines.

  2. その1ステップ計算を定義してください./ Please define their one-step computation.

  3. マシンが与えられた入力テープに対して停止するという述語を定義してください./ Please define the predicate that a machine halts on a given input tape.

  4. 長さ・内容不明のcyclicテープを入力し,テープをゼロクリアして停止するマシンを与えてください.テープ長の最小値を仮定してかまいません.このパズルは私が以前 Vincent van Oostrom先生より頂いたものです./ Please define a machine that, given an input cyclic tape of unknown size and content, clears the tape and halts. You may assume a minimum length on input tapes. This puzzle was given to me by Vincent van Oostrom.

  5. そのマシンに具体なテープを与え,動きを例示してください./ Please demonstrate how your machine above works on a concrete tape example.

  6. (任意) そのマシンが任意のcyclicテープに対して停止し,結果のテープがクリアされていることを証明してください./ (Optional) Please prove that your machine halts and resulting tape is cleared for any input cyclic tape.

解答 / Solutions

これまでのTPP / Past TPPs

TPP2018 / TPP2017 / TPP2016 / TPP2015 / TPP2014 / TPP2013 / TPP2012 / TPP2011 / TPP2010 / TPP2009 / TPP2008 / TPP2007 / TPP2006 / TPP2005