-
Notifications
You must be signed in to change notification settings - Fork 2
VerboseTableuxCalculus
George Plotnikov edited this page May 29, 2021
·
5 revisions
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()
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 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
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.
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
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
Functions