Formalization of proofs using relational calculus

Yoshihiro Mizoguchi; Hisaharu Tanaka; Shuichi Inokuchi

Formalization of proofs using relational calculus

Yoshihiro Mizoguchi, Hisaharu Tanaka, Shuichi Inokuchi

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Proceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	527-531
Number of pages	5
ISBN (Electronic)	9784885523090
Publication status	Published - Feb 2 2017
Event	3rd International Symposium on Information Theory and Its Applications, ISITA 2016 - Monterey, United States Duration: Oct 30 2016 → Nov 2 2016

Publication series

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

Other

Other	3rd International Symposium on Information Theory and Its Applications, ISITA 2016
Country/Territory	United States
City	Monterey
Period	10/30/16 → 11/2/16

All Science Journal Classification (ASJC) codes

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

Cite this

Mizoguchi, Y., Tanaka, H., & Inokuchi, S. (2017). Formalization of proofs using relational calculus. In 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).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Mizoguchi, Y, Tanaka, H & Inokuchi, S 2017, Formalization of proofs using relational calculus. in 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, United States, 10/30/16.

Mizoguchi Y, Tanaka H, Inokuchi S. Formalization of proofs using relational calculus. In 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",

note = "Publisher Copyright: {\textcopyright} 2016 IEICE.; 3rd International Symposium on Information Theory and Its Applications, ISITA 2016 ; Conference date: 30-10-2016 Through 02-11-2016",

year = "2017",

month = feb,

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.

T2 - 3rd International Symposium on Information Theory and Its Applications, ISITA 2016

Y2 - 30 October 2016 through 2 November 2016

ER -

Formalization of proofs using relational calculus

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this