The present study aims at a formalization of a deductive calculus for classical logic based on tableaux. The calculi DT, for propositional logic, and QDT, for predicate logic, are presented. A possible formaliation of an intuitionistic calculus on the same framework is conjectured. These calculi derive from a reformulation of Roderick Batchelor's Data Calculi, which are briefly presented at the beginning.

O presente estudo tem por objetivo a formalização de um cálculo dedutivo para a lógica clássica baseado em tableaux. São apresentados os cálculos DT, para a lógica proposicional, e QDT, para a lógica de predicados. Uma possível formalização de um cálculo intuicionista nos mesmos moldes é conjecturada. Esses cálculos derivam de uma reformulação do Cálculo de Dados de Roderick Batchelor, que é brevemente apresentado no início.