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
            sb.Append $"{value}\t" |> ignore
            let len = ((VerboseFormula formula).Length / 8)
            for _ = 1 to len do
                sb.Append "\t" |> ignore
        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(_) ->
                                sb.Append $"{rowVarValues.Item(j)} \t" |> ignore
                                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
                )
            sb.Append "\r\n" |> ignore
        sb.ToString()

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