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 | United States |
| City | Monterey |
| Period | 10/30/16 → 11/2/16 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Computer Networks and Communications
- Hardware and Architecture
- Information Systems
- Signal Processing
- Library and Information Sciences
Cite this
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
}
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 -