Programme
August 31, Sat
9:45 〜 10:00 Opening
10:00 ～ 12:00
1. Invited speaker: Shin-ya Katsumata (ERATO Hasuo Metamathematics for Systems Design Project, National Institute of Informatics)
Title: Mathematical Approaches to Cyber Physical Systems
Abstract: TBA
2. Devi Rahmah Sope (Kindai University)
Title: On a Fuzzification and Comparison of Clustering Indices
Abstract:
Fuzzy clustering is given by assigning to each data a set of membership degree to clusters. Quality of such a clustering is evaluated by measuring compactness and separateness. In crisp clustering, many clustering indices are proposed. In this article, we try to fuzzify these clustering indices by using membership degrees with higher order exponent and evaluate the effect in optimization problem.
3. Haruka Tomita (RIMS, Kyoto university)
Title: Constructing non-symmetric closed categories from planar combinatory algebra
Abstract:
In categorical realizability, we used to construct categories of assemblies and modest sets from (partially) combinatory algebras. We show that applying this construction to the planar lambda calculus and the corresponding combinatory algebras gives rise to closed categories, closed multi-categories and skew closed categories, which are structures weaker than Cartesian closed categories and symmetric monoidal closed categories. We give the necessary conditions and sufficient conditions on the combinatory algebras for obtaining these categorical structures.
12:00 ～ 14:00 Lunch
14:00〜15:30
1. Invited speaker: Takeuti Izumi(AIST)
Title: Mathematics and Variables
Abstract:
Mathematics has various usages of variables. There arise a question: Although mathematics has various kinds of variables, how did Frege banish such variables and represent mathematics by his predicate logic with only bound variables? In industrial words of the same question: How do we express various kinds of variables in formal proof systems, such as Coq, Isabelle, and so on, which have only free variables and bound variables? Analysing such usages and interpreting them into predicate logic have the following two significance. The first significance is an academic one. The analysis of usages of variables helps the studies of the histories of mathematics, logic and philosophy. By using the usages of variables as a clue, we can compare the theories by Aristotle, Leibniz and Frege. The other one is industrial. By proving mathematical theorems in formal proof systems, we can verify the specifications of softwares. This study shows the interpretations of various kinds of variables into predicate logic.
2. Shota Motoura (NEC Corporation)
Title: On Logic for Conditional Probabilities of Propositional Formulae
Abstract:
Popper proposed, in his work (Popper, 1959), a notion of conditional probability whose arguments are propositional formulae, which is called a Popper function. In this talk, we first explain that an instance of many-sorted monadic second-order logic can define the class of Popper functions, up to isomorphism. We then prove that, for any first-order formula in which any occurrence of a propositional formula is an argument of the predicate symbol for Popper function, it is decidable whether or not the formula is valid. At the end of the talk, we mention a technique to calculate the range of the value of a given conditional probability under given conditions expressed by such first-order formulae.
15:30 ～ 16:00 Break
16:00 ～ 17:30
1. Soichiro Fujii (RIMS, Kyoto University)
Title: Enriched categories and tropical mathematics
Abstract:
We point out a connection of enriched category theory over a quantale and tropical mathematics. Quantales or complete idempotent semirings, as well as matrices with coefficients in them, are fundamental concepts in both fields. We show that standard category-theoretic constructions on matrices, namely composition, right extension, right lifting and the Isbell hull, can unify various notions in tropical mathematics and related fields.
2. Koji Yasuda (Kanagawa University)
Title: Relationship among orders, semigroups, and quantales
Abstract:
Nishizawa and Furusawa showed a relational embedding of powerset quantales in RAMiCS 2012. To analyze the embedding, we studied the relationship among orders, semigroups, and quantales.
3. Koki Nishizawa (Kanagawa University)
Title: Correspondences among classes of weak preorders, partial semigroups, and quantales
Abstract:
Our goal is to extend the relational embedding of powerset quantales to a dual equivalence between the category of powerset quantales and the category of some class of preorders. In this talk, we define 6 pullbacks in Cat meaning correspondences among classes of weak preorders, partial semigroups, and quantales.
19:10 ～
Dinner @ 漁師小屋 We will welcome your joining. The registration is now closed. Please e-mail to kawamura AT inf.kyushu-u.ac.jp , OR nishizawa AT kanagawa-u.ac.jp.
September 1, Sun
of the satisfiability problem for constrained Horn clauses, and is polynomial-time equivalent to the verification problem. The latter is a remarkable properties that no existing logical approach has.
10:00 ～ 12:00
1. Invited speaker: Isamu Hasegawa (SQUARE ENIX CO., LTD.)
Title: Game development with ALGI
Abstract:
The workload of game development and quality assurance has increased along with upsizing of game in the recent video game industry. In order to ease those burden, we are trying to mix mathematics and computer science into the solutions so that we can automate some game development process that have been treated manually so far. In this session, we will introduce some examples that we are applying mathematics and computer science to game development such as the script verification by model checking.
2. Takeshi Tsukada (University of Tokyo)
Title: Fixed-Point Arithmetic and Program Verification
Abstract:
Program verification is a family of problems to decide if a given program satisfies a given specification. A major approach to problem verification is a logical approach that reduced the verification problem to a logical problem such as satisfiability, validity and model checking problems and then invokes a solver of the logical problem. This approach has been extensively studied for a class of specifications known as safety properties; the verification problem for this class can be naturally reduced to a well-known logical problem, the satisfiability problem of constrained Horn clauses. In this talk, we focus on a fairly general class of specifications, namely omega-regular properties, and see its tight connection to fixed-point arithmetic. The validity problem for fixed-point arithmetic is a natural extension
3. Hideki Tsuiki (Kyoto University)
Title: Program extraction from proofs on non-constructive objects
Abstract:
Extraction of programs from proofs about abstract mathematical objects. IFP (Intuitionistic Fixed Point Logic) is a logical system for program extraction developed by Ulrich Berger of Swansea University and his collaborators, and I am also engaged in the project.
IFP is a multi-sorted intuitionistic first order logic extended with induction and coinduction. In IFP, one can extract a program from a proof about abstract mathematical objects defined through axioms, like the set of real numbers. Here, abstract means that we do not fix a representation of an object and representation itself is also extracted from a proof. In this talk, we explain uniform treatment of quantifiers which is a fundamental idea that allows such treatment of mathematical objects, and show some examples of extraction.
12:00 ～ 14:00 Lunch
14:00 ～ 15:30
1. Invited speaker: Takanori Maehara (RIKEN Center for Advanced Intelligence Project)
Title: Submodular Maximization on Several Constraints specified by Algebra, Geometry, and Logic
Abstract:
A problem of approximately maximizing a submodular set function is a fundamental combinatorial optimization problem that has many applications in machine learning and data mining. Recently, we extended the problem to more complex domains such as lattices, complexes, and graphs with logics. In this presentation, we review the tractability of the problem from the viewpoint of the application of algebra, geometry, and logic.
2. Kohei Tanaka (Faculty of Economics and Law, Shinshu University)
Title: Topological and combinatorial methods in symmetric motion planning
Abstract:
The topological complexity is a numerical homotopy invariant introduced by M. Farber to study the robot motion planning. Farber and his coworkers also introduced the symmetric topological complexity taking symmetricity into account. In this talk, I will present a combinatorial approximation of the symmetric topological complexity and its refinement using loop-free categories.
15:30 ～ 16:00 Break
16:00 ～ 17:00
1. Yoriyuki Yamagata (AIST)
Title: Recent progress of consistency proofs of equational systems inside bounded arithmetics
Abstract:
We report some results extending a consistency proof of Cook and Urqhart’s PV minus induction inside S22.
17:00 ～ 17:15 Closing