Formalization of proofs using relational calculus

Yoshihiro Mizoguchi, Hisaharu Tanaka, Shuichi Inokuchi

研究成果: 著書/レポートタイプへの貢献会議での発言

抄録

We introduce a theory of relations and a method to prove using relational calculus. Several notions in mathematics and computer science are formalized using relational expressions. Propositions described by relational expressions can be solved by relational calculus, symbolic computations. We propose to apply our formalization to proofs in coding theory especially formalizations of algorithms including an error-correcting algorithm using automata. We introduce a formalization of notions in category theory and automata theory using relational expressions. We also show a formalization of an elementary theory of relations in Coq, a proof assistant system. We introduce an automatic proving procedures (tactics) for our formalization of the theory of relational calculus.

元の言語英語
ホスト出版物のタイトルProceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016
出版者Institute of Electrical and Electronics Engineers Inc.
ページ527-531
ページ数5
ISBN(電子版)9784885523090
出版物ステータス出版済み - 2 2 2017
イベント3rd International Symposium on Information Theory and Its Applications, ISITA 2016 - Monterey, 米国
継続期間: 10 30 201611 2 2016

出版物シリーズ

名前Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016

その他

その他3rd International Symposium on Information Theory and Its Applications, ISITA 2016
米国
Monterey
期間10/30/1611/2/16

Fingerprint

formalization
Automata theory
Computer science
computer science
assistant
tactics
coding
mathematics

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Hardware and Architecture
  • Information Systems
  • Signal Processing
  • Library and Information Sciences

これを引用

Mizoguchi, Y., Tanaka, H., & Inokuchi, S. (2017). Formalization of proofs using relational calculus. : Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016 (pp. 527-531). [7840480] (Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016). Institute of Electrical and Electronics Engineers Inc..

Formalization of proofs using relational calculus. / Mizoguchi, Yoshihiro; Tanaka, Hisaharu; Inokuchi, Shuichi.

Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016. Institute of Electrical and Electronics Engineers Inc., 2017. p. 527-531 7840480 (Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016).

研究成果: 著書/レポートタイプへの貢献会議での発言

Mizoguchi, Y, Tanaka, H & Inokuchi, S 2017, Formalization of proofs using relational calculus. : Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016., 7840480, Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016, Institute of Electrical and Electronics Engineers Inc., pp. 527-531, 3rd International Symposium on Information Theory and Its Applications, ISITA 2016, Monterey, 米国, 10/30/16.
Mizoguchi Y, Tanaka H, Inokuchi S. Formalization of proofs using relational calculus. : Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016. Institute of Electrical and Electronics Engineers Inc. 2017. p. 527-531. 7840480. (Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016).
Mizoguchi, Yoshihiro ; Tanaka, Hisaharu ; Inokuchi, Shuichi. / Formalization of proofs using relational calculus. Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016. Institute of Electrical and Electronics Engineers Inc., 2017. pp. 527-531 (Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016).
@inproceedings{3241c4e89d1a4ac287fbd1c8ab45ccae,
title = "Formalization of proofs using relational calculus",
abstract = "We introduce a theory of relations and a method to prove using relational calculus. Several notions in mathematics and computer science are formalized using relational expressions. Propositions described by relational expressions can be solved by relational calculus, symbolic computations. We propose to apply our formalization to proofs in coding theory especially formalizations of algorithms including an error-correcting algorithm using automata. We introduce a formalization of notions in category theory and automata theory using relational expressions. We also show a formalization of an elementary theory of relations in Coq, a proof assistant system. We introduce an automatic proving procedures (tactics) for our formalization of the theory of relational calculus.",
author = "Yoshihiro Mizoguchi and Hisaharu Tanaka and Shuichi Inokuchi",
year = "2017",
month = "2",
day = "2",
language = "English",
series = "Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "527--531",
booktitle = "Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016",
address = "United States",

}

TY - GEN

T1 - Formalization of proofs using relational calculus

AU - Mizoguchi, Yoshihiro

AU - Tanaka, Hisaharu

AU - Inokuchi, Shuichi

PY - 2017/2/2

Y1 - 2017/2/2

N2 - We introduce a theory of relations and a method to prove using relational calculus. Several notions in mathematics and computer science are formalized using relational expressions. Propositions described by relational expressions can be solved by relational calculus, symbolic computations. We propose to apply our formalization to proofs in coding theory especially formalizations of algorithms including an error-correcting algorithm using automata. We introduce a formalization of notions in category theory and automata theory using relational expressions. We also show a formalization of an elementary theory of relations in Coq, a proof assistant system. We introduce an automatic proving procedures (tactics) for our formalization of the theory of relational calculus.

AB - We introduce a theory of relations and a method to prove using relational calculus. Several notions in mathematics and computer science are formalized using relational expressions. Propositions described by relational expressions can be solved by relational calculus, symbolic computations. We propose to apply our formalization to proofs in coding theory especially formalizations of algorithms including an error-correcting algorithm using automata. We introduce a formalization of notions in category theory and automata theory using relational expressions. We also show a formalization of an elementary theory of relations in Coq, a proof assistant system. We introduce an automatic proving procedures (tactics) for our formalization of the theory of relational calculus.

UR - http://www.scopus.com/inward/record.url?scp=85015180222&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85015180222&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:85015180222

T3 - Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016

SP - 527

EP - 531

BT - Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016

PB - Institute of Electrical and Electronics Engineers Inc.

ER -