分野別セミナー

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 mathematics about a theory of relations has been existing for a long while. In this talk, we review those theory of relations and methods 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 using relational calculus, symbolic computations. 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.