Press-ready deduction trees in classical logic using point-plus-expressions. The 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 advantage of the connection between resolution and its dual, and then the connection between sequent calculus and the tableau method.

References in zbMATH (referenced in 1 article , 1 standard article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Kádek, Tamás: Press-ready deduction trees in classical logic using point-plus-expressions (2012)