Software in Mathematics Demonstration Track in Hakata Workshop 2017
Hakata Workshop(博多ワークショップ)~Discrete Mathematics and its Applications
九州大学 マス・フォア・インダストリ研究所
数学理論先進ソフトウェア開発室
Software in Mathematics Demonstration Track in Hakata Workshop 2017
Hakata Workshop(博多ワークショップ)~Discrete Mathematics and its Applications
九州大学 マス・フォア・インダストリ研究所
数学理論先進ソフトウェア開発室
Constructor-based Inductive Theorem Prover (CITP) is a proof management tool built on top of an algebraic specification language. This means that there exists a intimate connection between the modeling technique and the verification approach. The methodology supported by the tool is not intended for formalizing mathematics, but for the application to the development of software systems. In order to achieve the targeted goal, two important research directions are pursued:
(1) proposing more expressive logical systems to allow engineers to specify easily and accurately the software systems, and
(2) develop decision procedures that can reason efficiently about these more sophisticated logics.
The CITP's source code has been refactored to be more readable and improved to make it a better platform for future extensions. The command parsing component was reimplemented to generate better error messages.
pdf file
It is well-known that for a finite group G the association scheme G can be obtained by its regular action. In this talk a finite group G is called desirable if for any symmetric fusion scheme of the association scheme of G is integral. Observing the one-to-one correspondence between the set of fusion schemes of the association scheme of G and the set of Schur rings over G, we will give demonstrations of finding finite desirable groups of small order by using GAP with COCO2p package.
変形行列を用いた補間ではARAP(As rigis as possible)と呼ばれる剛性を保 持するような補間アルゴリズムがある. 本モジュールはARAPの補間法を用いた2 次元のポリゴン図形の描画, 移動や補間 のためのMathematicaモジュールである. このモジュールでは, 大域補間は局所補間, エラー関数, 制約関数から決まり, いくつかある関数の中からユーザーが選択し設定することができる. モジュール中の展開された式を用いた補間を計算する関数は,C 言語のように記 号計算の関数を持たない他の言語においても使うことができる. 本モジュールを使うことで補間の重要な例について, 分析や調査をすることがで きる. Mathematica モジュール中の関数を使用して, 局所エラー関数や制約関数 の二次形式表現を数式のまま求めることができる.
セイバーメトリクスで知られている野球のスポーツデータ解析において、 本研究では投手の評価指標に注目する。 これまで主として用いられている防御率は客観的な指標でないことや 一般に救援投手に有利な評価指標となっている。 本研究では統計的手法を用いることで投手タイプを客観的な指標のみで分類した。 そこでは複数のタイプに属することを許すFuzzyクラスタリングを行うことで これまでにない柔軟な分類ができた。 また、そのタイプを考慮することで各グループごとに線形重回帰分析を行い、 防御率の弱点を克服した客観的な投手評価手法を構築した。 これらの分析には統計解析ソフトRを用いた。
Since National Security Agency (NSA) announced the plans for
transitioning to the algorithms, which are resistant to attacks by the
potential quantum computers, the interest of implementation of post-
quantum cryptography (PQC) on various platforms has emerged. In recent
years, lattice-based cryptography has attracted a high degree of
attention in the cryptologic research community. It is expected to be in
wide use in the foreseeable future once large quantum computers are in
sight. On the other hand, JavaScript is a standard programming language
for Web applications. It is now supported on a wide variety of computing
platforms and devices with immense efficiency improvement in the past
few years.
Meanwhile, including widely used Java Card, memory-constrained smart
cards need the efficient implementation of encryption schemes to resist
quantum-computing attacks. We present the results of our implementation
of several lattice-based encryption schemes and show the speed
performance on four common Web browsers on PCs. Furthermore, we show
performance results on three smaller computing platforms, namely,
tablets running the Android operating system, Tessel which is an
embedded system equipped with an ARM Cortex M3 microcontroller, as well
as Java Card.
Our results demonstrate that some of today’s lattice-based cryptosystems
can already have efficient JavaScript implementations and hence are
ready for use on a growing list of computing platforms with JavaScript
support. Moreover, we indicate that polynomial multiplication and over
signed 16-bit integer arithmetic can be performed on Java Card even if
the unsigned short type and integer type are not supported, which makes
running more lattice-based protocols on Java Card achievable.
article
3次元ユークリッド空間における曲面の第一基本形式を保つ変形を等長変形という，第一基本形式のみの情報によって決定される不変量を内的不変量と呼び，等長変形によって変化し得る不変量を外的不変量と呼ぶ． 例えば，曲面上の一点 p において，接平面に直交する平面による切り口として 得られる曲線の曲率の最大値と最小値を点 p における主曲率といい，外的不変量である．一方で，この2つの主曲率の積を「ガウス曲率」と呼び，定義上は外的な量を用いているように見える．しかし，実際は，ガウス曲率は第一基本形式のみよって記述される内的な不変量であり，この事実は「ガウスの驚異定理」として広く知られている． 本発表では，Mathematica を用いて，リーマン幾何でしばしば登場する種々の曲率を含む不変量を記号的に計算するプログラムを開発したこと，および，曲面論の研究において，それを実際にどのように用いているのかを説明する．また，一つのデモンストレーションとして，上述の「ガウスの驚異定理」が成り立つことを Mathematica を用いて証明する．
本研究はグラフの距離を出来るだけ保存するようなユークリッド空間への埋め込みを考えている. しかし，数学的にそのような最善の埋め込みを求めることは一般には大変難しい． そこで，グラフのユークリッド空間への最善の埋め込みを決定する問題をある半正定値計画法を解くことに帰着し， MATLABのSeDuMi を用いて5頂点以下のグラフに対して最 善の埋め込みを計算する. しかし，その計算は近似計算であるため数学的に厳密に埋め込みが最善であることを決定しているわけではない. そこで，この問題に対する解答として上記の計算結果及び半正定値計画問題の弱双対定理を応用することで 最善の埋め込みを厳密な形で求める方法について議論する.