VerboseTableuxCalculus

        let VerboseTableuxCalculus (formulaCalcList: Formula list) (formulaInterpritations: bool list list) : string =
        let sb = new System.Text.StringBuilder()
        let subFormulasVals = new Dictionary<Formula, bool>()

        let _saveFormulaValueAndPrint =
            fun formula value ->
                if not (subFormulasVals.ContainsKey(formula)) then
                    subFormulasVals.Add(formula, value)
                else
                    subFormulasVals.Item(formula) <- value

                bprintf sb $"{value}\t"
                let len = ((VerboseFormula formula).Length / 8)

                for _ = 1 to len do
                    bprintf sb "\t"

        for i = 0 to formulaInterpritations.Length - 1 do
            let rowVarValues = formulaInterpritations.Item i
            let mutable j = 0

            formulaCalcList
            |> List.iter (fun f ->
                match f with
                | Formula.Var (_) ->
                    bprintf sb $"{rowVarValues.Item(j)} \t"
                    j <- j + 1
                | Formula.Neg (Var (x)) ->
                    let index =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(x))

                    let calc = CalcFormula(Formula.Neg(Formula.Const(rowVarValues.Item(index))))
                    _saveFormulaValueAndPrint f calc
                | Formula.Conj (Var (x), Var (y)) ->
                    let indexX =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(x))

                    let indexY =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(y))

                    let calc =
                        CalcFormula(Conj(Const(rowVarValues.Item(indexX)), Const(rowVarValues.Item(indexY))))

                    _saveFormulaValueAndPrint f calc
                | Formula.Disj (Var (x), Var (y)) ->
                    let indexX =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(x))

                    let indexY =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(y))

                    let calc =
                        CalcFormula(Disj(Const(rowVarValues.Item(indexX)), Const(rowVarValues.Item(indexY))))

                    _saveFormulaValueAndPrint f calc
                | Formula.Bic (Var (x), Var (y)) ->
                    let indexX =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(x))

                    let indexY =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(y))

                    let calc =
                        CalcFormula(Bic(Const(rowVarValues.Item(indexX)), Const(rowVarValues.Item(indexY))))

                    _saveFormulaValueAndPrint f calc
                | Formula.Bic (Var (x), y) ->
                    let rightVal = subFormulasVals.GetValueOrDefault(y)

                    let indexX =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(x))

                    let calc = CalcFormula(Bic(Const(rowVarValues.Item(indexX)), Const(rightVal)))
                    _saveFormulaValueAndPrint f calc
                | Formula.Bic (x, Var (y)) ->
                    let leftVal = subFormulasVals.GetValueOrDefault(x)

                    let indexY =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(y))

                    let calc = CalcFormula(Bic(Const(rowVarValues.Item(indexY)), Const(leftVal)))
                    _saveFormulaValueAndPrint f calc
                | Formula.Bic (x, y) ->
                    let leftVal = subFormulasVals.GetValueOrDefault(x)
                    let rightVal = subFormulasVals.GetValueOrDefault(y)
                    let calc = CalcFormula(Bic(Const(rightVal), Const(leftVal)))
                    _saveFormulaValueAndPrint f calc
                | Formula.Impl (Var (x), Var (y)) ->
                    let leftVal =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(x))

                    let rightVal =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(y))

                    let calc =
                        CalcFormula(Impl(Const(rowVarValues.Item(leftVal)), Const(rowVarValues.Item(rightVal))))

                    _saveFormulaValueAndPrint f calc
                | Formula.Impl (x, Var (y)) ->
                    let leftVal = subFormulasVals.GetValueOrDefault(x)

                    let rightVal =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(y))

                    let calc = CalcFormula(Impl(Const(leftVal), Const(rowVarValues.Item(rightVal))))
                    _saveFormulaValueAndPrint f calc
                | Formula.Impl (Var (x), y) ->
                    let rightVal = subFormulasVals.GetValueOrDefault(y)

                    let leftVal =
                        formulaCalcList
                        |> List.findIndex (fun h -> h = Var(x))

                    let calc = CalcFormula(Impl(Const(rowVarValues.Item(leftVal)), Const(rightVal)))
                    _saveFormulaValueAndPrint f calc
                | Formula.Impl (x, y) ->
                    let leftVal = subFormulasVals.GetValueOrDefault(x)
                    let rightVal = subFormulasVals.GetValueOrDefault(y)
                    let calc = CalcFormula(Impl(Const(leftVal), Const(rightVal)))
                    _saveFormulaValueAndPrint f calc
                | _ -> printf "unknown formula %A" f)

            bprintf sb "\r\n"

        sb.ToString()

This formula calculates trivial formulas and builds string output in the table view. Trivial formulas calculation is performed by using CalcFormula method.

There is one inner method:

        let _saveFormulaValueAndPrint =
            fun formula value ->
                if not (subFormulasVals.ContainsKey(formula)) then
                    subFormulasVals.Add(formula, value)
                else
                    subFormulasVals.Item(formula) <- value

                bprintf sb $"{value}\t"
                let len = ((VerboseFormula formula).Length / 8)

                for _ = 1 to len do
                    bprintf sb "\t"

Then it does iterates through all possible interpretations and saves the output as a string. To find a particular Variable value it searches for let leftVal = formulaCalcList |> List.findIndex(fun h -> h = Var(x)) index of the Variable and make up an Atom Impl(Const(rowVarValues.Item(leftVal)) and then evaluates by CalcFormula method.

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 output =  VerboseTableuxCalculus formulaCalcList formulaInterpritations