Header menu logo F# Header menu logo Averest

SequentProofTree Type

type for sequent calculus proof trees; each node has either one, two or no successor nodes and consists of two sets of formulas. Moreover, each node is uniquely identified by an index. Leaf nodes are further separated into valid ones (NodeTrue) and invalid ones (NodeFalse).

Union cases

Union case Description
Item : int * Set<BoolExpr> * Set<BoolExpr> * SequentProofTree
Item : int * Set<BoolExpr> * Set<BoolExpr> * SequentProofTree * SequentProofTree

NodeFalse int * Set<BoolExpr> * Set<BoolExpr>

Full Usage: NodeFalse int * Set<BoolExpr> * Set<BoolExpr>

Parameters:
Item : int * Set<BoolExpr> * Set<BoolExpr>

NodeTrue int * Set<BoolExpr> * Set<BoolExpr>

Full Usage: NodeTrue int * Set<BoolExpr> * Set<BoolExpr>

Parameters:
Item : int * Set<BoolExpr> * Set<BoolExpr>

Instance members

Instance member Description

this.IsNodeAlpha

Full Usage: this.IsNodeAlpha

Returns: bool
Returns: bool

this.IsNodeBeta

Full Usage: this.IsNodeBeta

Returns: bool
Returns: bool

this.IsNodeFalse

Full Usage: this.IsNodeFalse

Returns: bool
Returns: bool

this.IsNodeTrue

Full Usage: this.IsNodeTrue

Returns: bool
Returns: bool

Type something to start searching.