Press-ready deduction trees in classical logic using point-plus-expressions

Abstract. The \({\rm \LaTeX}\) system is widely used in scientific journals with syntactically rich mathematical expressions. It is suitable not only for high-quality press-ready production, but it can also be applied for the development of dynamic presentations and learning materials containing many nice formulas. The need to construct numerous derivations using Gentzen style sequent calculus, gives the idea to automatize the process (which was implemented in the GenTreeCad application). The point-plus-expressions show how to use an existing derivation to produce different solutions by different theorem proving methods.
In this artice, we try to demonstrate the capability of point-plus-expressions meanwhile we are using them for automatic theorem proving. We want to show — using propositional logic — how we could take the advantages of the connection between the resolution and it is dual one, then the connection between sequent calculus and the tableau method as well.