Formalização do Cálculo Pointfree em estilo relacional

A Lógica de Primeira Ordem provê técnicas para demonstrar e expressar propriedades de correção sobre sistemas. Entretanto, especificação e formalização são técnicas que tomam muito tempo na construção de software e hardware. Logo, o objetivo é estudar um mecanismo alternativo de especificação e dedução baseado em álgebra relacional, chamado cálculo relacional, e compará-lo com o cálculo de Gentzen, observando tamanhos de provas e de especificações. _____________________________________________________________________________ ABSTRACTThe First Order Logic provides techniques to demonstrate and express properties of correctness in systems. However, specification and formalization are techniques that take a lot of time in the construction of software and hardware. Thus, the goal is to study an alternative way of deduction and specification based on relational algebra, called relational calculus, and to compare to Gentzen calculus, seeing sizes of proofs and specifications