Sabe-se que o wittgensteiniano ver aspectos está intrinsecamente relacionado com a atividade matemática -- ao menos isso fica bastante claro no caso da geometria. No caso da álgebra, contudo, as coisas não são tão evidentes. Foi em um artigo de 1996 que Curtis e Lowe aprofundaram essa ideia ao proporem traduzir proposições matemáticas em termos de grafos. Nesse contexto, motivados pela expressividade dessa nova linguagem, os autores formularam um cálculo relacional orientado a fluxo para predicados binários e mostraram como as famosas sentenças de Lyndon podem ser facilmente derivadas. Contudo, questões fundamentais como consistência e completude foram deixadas para trabalhos futuros. Mais recentemente, no artigo 'On graph reasoning' (2009), as mesmas ideias de 1996 foram retomadas. Nesse artigo, os autores introduziram a linguagem +RG e demonstraram a sua consistência e completude (fraca) com relação ao cálculo relacional positivo. Desde então, no esforço de desenvolver as ideias seminais de Curtis e Lowe, novos trabalhos surgiram nesse mesmo sentido. Neste seminário, pretendo ilustrar como a relação de consequência pode ser compreendida em termos de homomorfismo entre grafos, avaliando a possibilidade de incorporar tal mecanismo em assistentes de prova. Para isso, irei sugerir a construção de algoritmos voltados para a derivação e decisão e esboçarei uma análise a complexidade computacional envolvida na tarefa.