Calculate a formula in tableaux method

let frm = Formula.Impl(Conj(Var "P", Var "Q"), Bic(Var "R", Neg(Var "S")))
let formulaCalcList =
    BuildFormulaCalcList frm
    |> List.sortBy (fun f -> CalcFormulaDepth f)

let formulaInterpritations = BuildAllFormulasInterpritations formulaCalcList

let result =  VerboseTableuxCalculus formulaCalcList formulaInterpritations

To build up a calculus for a formula in the tableaux method there is necessary to perform several steps:

1. Define a formula
2. Get a list of calculus from the formula (see this function)
3. Build all formulas interpretations (see this function)
4. Calculate all interpretations of the formula and show it in a table view.

Example

Input:

Formula.Impl(Conj(Var "P", Var "Q"), Bic(Var "R", Neg(Var "S")))

Output:

P       Q       R       S       ~S      (P && Q)        (R <=> ~S)      ((P && Q) -> (R <=> ~S))        
True    True   True     True    False   True            False           False
True    True    True    False   True    True            True            True
True    True    False   True    False   True            True            True
True    True    False   False   True    True            False           False
True    False   True    True    False   False           False           True
True    False   True    False   True    False           True            True
True    False   False   True    False   False           True            True
True    False   False   False   True    False           False           True
False   True    True    True    False   False           False           True
False   True    True    False   True    False           True            True
False   True    False   True    False   False           True            True
False   True    False   False   True    False           False           True
False   False   True    True    False   False           False           True
False   False   True    False   True    False           True            True
False   False   False   True    False   False           True            True
False   False   False   False   True    False           False           True

Usage

let frm = Formula.Impl(Conj(Var "P", Var "Q"), Bic(Var "R", Neg(Var "S")))
let formulaCalcList =
    BuildFormulaCalcList frm
    |> List.sortBy (fun f -> CalcFormulaDepth f)

let formulaInterpritations = BuildAllFormulasInterpritations formulaCalcList

let result =  VerboseTableuxCalculus formulaCalcList formulaInterpritations