Speaker: Petrucio Viana (Institute of Mathematics and Statistics, Federal Fluminense University, Brazil)
Title: Graph calculus for proving equations and inclusions true on allegories
Abstract:
Traditionally, formulas are written on a single line. S. Curtis and G. Lowe suggested a more visually appealing alternative for the case of binary relations: using graphs for expressing properties and reasoning about relations in a natural way. We extended their approach to diagrams that are sets of graphs.
More specifically, in this setting, diagrams corresponds to sentences and transformations on graphs diagrams correspond to inference rules, that can be used to infer a diagram from a set of diagrams taken as hypothesis. The basic intuitions are quite simple, leading to playful and powerful systems. Our system fits very well as a tool for perform inferences on algebras of binary relations, but we developed it to treat positive, negative, and intuitionistic information, ranging from the geometric fragment to the whole of first order logic on binary relations.
In this talk I summarize these achievements, presenting some on going work on extending the previous systems to deal with the equations and containments of the distributive, division, and power allegories, being tabular or not. Given the connection between classical modal logics and algebras of relations developed by E. Orlowska and her collaborators, our graphical system may be also explored as a tool for perform inferences in modal logic.