A LaTeX package to typeset formal proofs and rules in the style of sequent calculus. This is an extended work of ebproof.
The ebproof package provides an ergonomic and scalable interface for typesetting proof trees. However, it has been a long-standing issue to stack hypotheses using ebproof (here and here).
Moreover, I believe this will reduce, if not resolve, a need to make ebproof compatible with the mathpartir environment (here and here).
The ebproofx
package is a non-breaking extension upon the ebproof
package with the following extras:
- Extends the
infer
macro to accept comma-separated lists of numbers, instead of a single number, to gather hypotheses in multiple lines. For instance,\infer{1,2,3}{X}
will stack six hypotheses, and break them into groups containing one, two, and three hypotheses. - The
InfRule
environment, which enables typesetting the rule name above the inference rule.
ebproofx is available under The LaTeX Project Public License 1.3. See the LICENSE file for more info.