Graph calculi for relational reasoning

Renata de Freitas and Petrucio Viana

Department of Mathematics and Statistics
Federal Fluminense University, Niteroi, Brazil

 

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 diagram taken as hypothesis. The basic intuitions are quite simple, leading to playful and powerful systems. Our systems treat positive, negative, and intuitionistic information.

In this minicourse we summarize these achievements, presenting proper formulations of these systems as logical calculi and discussing soundness, completeness and decidability.

The course has no pre-requisites besides some familiarity with formal reasoning and with the basic logic ideas on the syntax and semantics of formal systems. Besides, all the necessary background will be presented as necessary.

 

 

 

 

 

 

Bibliography

Renata de Freitas and Petrucio Viana. 
A graph calculus for proving intuitionistic relation algebraic equations. 
Diagrams 2012, LNCS 7352:324-326 (2012). 

Renata de Freitas, Paulo A.S. Veloso, Sheila R.M. Veloso, and Petrucio Viana. 
A calculus for graphs with complement. 
Diagrams 2010, LNCS 6170:84-98 (2010). 

Renata de Freitas, Paulo A.S. Veloso, Sheila R.M. Veloso, and Petrucio Viana. 
On graph reasoning. 
Information and Computation 207:1000-1014 (2009). 

Renata de Freitas, Sheila R.M. Veloso, Paulo A.S. Veloso, and Petrucio Viana. Positive Fork Graph Calculus. LFCS'09, LNCS 5407:152-163 (2009)

Renata de Freitas and Petrucio Viana. 
A note on proofs with graphs. 
Science of Computer Programming 73:129-135 (2008). 

�>