Room 11408 of Building 11, Kyoto Sangyo University
Motoyama, Kamigamo, Kita-ku, Kyoto, 603-855
Day
September 12, 2015, 13:00–18:00
Organizers
Masayuki Noro (Rikkyo University)
Nobuki Takayama (Kobe University)
Tatsuyoshi Hamada (Fukuoka University / OCAMI)
Shun-ichi Yokoyama (Kyushu University / CREST)
Support
MSJ Committee for Network Administration
Speaker (Alphabetical order)
Kato, Kimikazu
Kawabe, Haruyuki
Kawazoe, Mitsuru and Yoshitomi, Kentaro
Mizoguchi, Yoshihiro
Preining, Norbert
Program
13:00-13:50 “Web-based learning/assessment systems for college mathematics developed with webMathematica” Mitsuru Kawazoe (Osaka Pref. University) and Kentaro Yoshitomi (Osaka Pref. University)
14:00-14:50 “Algebraic specifications and Functional programming with CafeOBJ” Norbert PREINING (Japan Advanced Institute of Science and Technology, Software Verification Center)
15:00-15:50 “The Coq Proof Assistant System” Yoshihiro Mizoguchi (Kyushu University / JST CREST)
16:00-16:50 “How to draw combinatorial geometric figures using TeX” Haruyuki Kawabe (Nihon Unisys, Ltd. Technology Research & Innovation)
17:00-17:50 “Mechanism and algorithms of recommendation system” Kimikazu Kato (Silver Egg Technology Co., Ltd.)
Abstract
13:00-13:50 “Web-based learning/assessment systems for college mathematics developed with webMathematica” Mitsuru Kawazoe (Osaka Pref. University) and Kentaro Yoshitomi (Osaka Pref. University)
With webMathematica, we have developed a web-based learning system and a web-based assessment system for college mathematics. Materials of both systems cover all topics in the standard courses of calculus and linear algebra, and more than 700 students use these systems every year. In this talk, we describe the features of both systems.
14:00-14:50 “Algebraic specifications and Functional programming with CafeOBJ” Norbert PREINING (Japan Advanced Institute of Science and Technology, Software Verification Center)
CafeOBJ is an algebraic specification language based on equational order-sorted logic, which incorporates rewriting logic and hidden algebras. What sets it apart from other specification languages is that it is also executable, means that specifications can be `executed’ or rewritten to prove properties. Furthermore, its flexible mix-fix syntax, powerful module system including inheritance and parametrized modules, it has the potential to function efficiently in various circumstances, including symbolic and algebraic computations.
In this talk we give a short introduction to CafeOBJ, go through a few examples of functional programming with CafeOBJ, and present an example of an algebraic specification and verification of its properties.
15:00-15:50 “The Coq Proof Assistant System” Yoshihiro Mizoguchi (Kyushu University / JST CREST)
Coq is a formal proof management system developed in the French Institute for Research in Computer Science and Automation (INRIA).
Recently there are several formal proofs of pure Mathematics using Coq.
In this talk, we first introduce how to start using Coq followed by an explanation of difference between a formal proof
and a usual proof. We use several elementary examples to show benefits of Coq.
16:00-16:50 “How to draw combinatorial geometric figures using TeX” Haruyuki Kawabe (Nihon Unisys, Ltd. Technology Research & Innovation)
Polyominoes are shapes made by connecting certain numbers of equal-sized
squares, each joined together with at least one other square along an edge.
Polyiamonds and Polyhexes are similar objects connecting equilateral traiangles
and regular hexagons, respectively. In this talk, we introduce how to draw those
combinatorial geometirc figures using TeX without/with some packages, such
as PSTricks and TikZ.
17:00-17:50 “Mechanism and algorithms of recommendation system” Kimikazu Kato (Silver Egg Technology Co., Ltd.)
This talk explains the mechanism of the recommendation system of shopping sites in the Internet, and introduces its algorithms used there. Looking at the difference from the rating prediction problem of a review site, we rationalize the difference of mathematical interpretations, and then explore some related research papers.
