IsFormulaAcceptable

    let IsFormulaAcceptable formula =
        match formula with
        | Var(n) -> true
        | Neg(n) -> true
        | Conj(Const(n), m) -> true
        | Conj(n, Const(m)) -> true
        | Conj(n, m) -> true
        | Disj(Const(n), m) -> true
        | Disj(n, Const(m)) -> true
        | Disj(n, m) -> true
        | Bic(n, m) -> true
        | Impl(n, m) -> true
        | _ -> false

IsFormulaValid function determines whether a formula is valid based on the definition from the Symbolic Logic and Mechanical Theorem Proving.

Definition Well-formed formulas, or formulas for short, in the propositional
logic are defined recursively as follows :
1. An atom is a formula.
2. If G is a formula, then ( ~ G) is a formula.
3. If G and H are formulas, then (G Λ H), (G V H), (G → H), and
(G ⇔ H) are formulas.
4. All formulas are generated by applying the above rules. 

Basically, the syntax doesn't allow to make an invalid formula. Nevertheless, this function must be, to make sure the formula to be used is valid and the system is robust and doesn't allow to make an error.

Example

Input:

    let frm = Formula.Impl(Conj(Var "P", Var "Q"), Bic(Var "R", Neg(Var "S")))
    let isFormulaValid = IsFormulaValid frm

Output: true

Usage

    let frm = Formula.Impl(Conj(Var "P", Var "Q"), Bic(Var "R", Neg(Var "S")))
    let isFormulaValid = IsFormulaValid frm
    printf $"Formula is valid: [{isFormulaValid}]"