|
Abstract |
There are many network structures (relations between certain objects) considered in applications of mathematics for industry. We use many calculations of numbers and equations of numbers in mathematical analysis. But we seldom use calculations of network structures or equations of relational structures. On the other hand, a sufficiently developed theory of relations has been existing for a long while. In this talk, we review those theory of relations from a view point of a computation. we show an elementary theory of relations and its formalization in Coq, a proof assistant system. Further, we introduce an automatic proving procedures (tactics) for our formalization of the theory of relational calculus. |
