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:

    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

Output:

Usage