九州大学 論理と計算研究室 関係計算の形式化を用いた数学とソフトウェア検証のための理論構築

数学ソフトウェア等

関係計算の形式化等に関わる過去からの数学ソフトウェア等を本ページに一覧にまとめる.

論理式表現された問題を混合整数計画問題へ自動変換する
ALLC(Automatic Logical formula to Linear equation Compiler)

論理式表現された問題を混合整数計画問題へ自動変換するシステムの開発, 平河尭, 2017.
Mathematicaを用いた共形幾何代数を用いた折紙系の定式化

Origami System using Conformal Geometric Algebra, M.Kondo, T.Matsuo, Y.Mizoguchi, H.Ochiai, 2015.
Mathematicaを用いたARAP剛体変形計算モジュール

Mathematica Module for two-dimensional computer graphics – Data structure and Interpolation algorithms -, T.Hirano, 2016.
線形WangタイルアルゴリズムのC++言語による実現

A linear algorithm for Brick Wang tiling, A.D-Jourdan, S.Kaji, Y.Mizoguchi, 2019.
線形WangタイルアルゴリズムのCoqによる検証

A certificated Wang tiling program with the Coq proof assistant, T.Matsushima, Y.Mizoguchim A.D-Jourdan, 2015.
剛板の曲線切断のための線分と円弧による近似アルゴリズムの実現

An approximation of a curve using line segments and arcs, A.Hirakawa, Y.Onitsuka, C.Matsufuji, D.Yamaguchi, S.Kaji, 2017.
Mathematicaを用いたグラフラプラシアンの固有値を用いたデータ分割計算モジュール

Bipartition of graphs based on normalized cut and spectral methods, K.K.K.R.Perera, Y.Mizoguchi, 2013.
定理証明支援系Coq例題集

Coqチュートリアル, 溝口佳寛, 2015.
Coqを用いた関係計算による定理証明支援モジュール

A Coq Library for Interactive Formal Theorem Proving in the Theory of Relational Calculus, T.Matsushima, 2015.
Mathematicaによるファジー関係データベース計算モジュール

A formalization of a fuzzy relational database model using relational calculus, M.D.Akbar, Y.Mizoguchi, 2016.
PAGE TOP