This package contains the classes {@link de.uka.iti.pseudo.proof.Proof} and {@link de.uka.iti.pseudo.ProofNode} that are used to represent proof trees. {@link de.uka.iti.pseudo.proof.RuleApplication}s are used to denote applications of rules in certain situations.

This package has some package private methods which are, e.g. shared between Proof and ProofNode. The publicly available interface is available from Proof rather than from ProofNode. The latter has only public getter methods, no setter methods.

Proof is thread-safe because of a locking mechanism (see {@link de.uka.iti.pseudo.proof.Proof}).

RuleApplication can be immutable or mutable. An immutable copy is made when a rule application is to be stored in a proof node.