分野別セミナー

An inductive definition is a way to define a predicate by an expression which may contain the predicate itself. The predicate is interpreted by the least fixed point of the defining equation. Inductive definitions are important in computer science, since they can define useful recursive data structures such as lists and trees. Inductive definitions are important also in mathematical logic, since they increase the proof theoretic strength. Martin-Lof's system of inductive definitions given in 1971 is one of the most popular system of inductive definitions.
In 2006 Brotherston proposed an alternative formalization of inductive definitions, called a cyclic proof system. In general, for proof search, a cyclic proof system can find an induction formula in a more efficient way than Martin-Lof's system, since a cyclic proof system does not have to choose fixed induction formulas in advance. The equivalence of the provability of Martin-Lof's system for inductive definitions and that of the cyclic proof system was conjectured in 2006. The speaker and Berardi solved it in 2017. This talk will explain this problem from basic background knowledge to the latest results.

Zoomオンライン参加登録URL
開催日時: 2022年3月10日 11:00 AM (日本)
https://us02web.zoom.us/meeting/register/tZcld-6tqzMiGdZPmIqw48OIdK25p0MtMjy6
登録後、ミーティング参加に関する情報の確認メールが届きます。