Seminario del prof. Makoto Tatsuta - 17 novembre 2025 ore 10:00

Lunedì 17 Novembre, alle ore 10:00, in Aula F il prof. Makoto Tatsuta del National Institute of Informatics - Sokendai, Japan terrà un seminario dal titolo "Brotherston's Conjecture: Equivalence of Inductive Definitions and Cyclic Proofs"

Abstract:
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.