Template:Proof tree

Write derivation trees. See the the documentation of the template for the detailed syntax.

Template parameters[Edit template data]

This template prefers block formatting of parameters.

Parameter		Description	Type	Status
Inline mode	inline	Whether the derivation tree should be written inline. This is mostly intended for writing several trees and centering them altogether.	Boolean	optional

Idea

It works similarly as the ebproof LaTeX package: hypotheses a pushed on a stack, and then popped to form inferences that are in turn pushed on the stack. When the process is finished, there should remain only one element on the stack: the complete proof tree, that is printed.

Syntax

The syntax is as follows:

{{Proof tree
| command argument1 argument2 ... content
| command argument1 argument2 ... content
| ...
}}

There are currently two commands (besides the inline parameter described above):

• hypo takes no argument and pushes its content on the stack.
• infer has the following syntax: infer n style:(...) label:(...) content, where:
  • the mandatory argument n is an integer telling how many premises the inferences needs (and will therefore be popped from the stack),
  • the optional argument style can be given the value double to produce a double-line inference,
  • the optional argument label can be given mathematical content, to be printed next to the inference.

In both cases, content is mathematical content that will be rendered via KaTeX (see explanations on math typesetting).