It defines the type of a PL formula which can be a *Literal*, *Double Negation*, *Alpha*, *Beta*, *Insat* or *Taut*

Defines the PL Semantic Tableau type as a Graph whose node labels are pairs of an integer (0: internal node, 1: open leaf, -1: closed leaf) and the PL set considered in the corresponding node; and the edge labels are defined as pairs of the applied rule (A, B, DN, L, I, T) and the list of indexes of the formulas on which the rule is applied.

It gives the type of a PL formula. Atoms and their negations are literals, double negation are typed as DN, conjunction, equivalence are classified as ALPHA, as well as disjunction and implications are classified as BETA. The negation of an alpha formula is a beta and vice versa.

f1 : FormulaPL
f1 = Atom "a"


f2 : FormulaPL
f2 = Atom "b"


fplType f1 == L
fplType (Neg f1) == L
fplType (Neg (Neg f1)) == DN
fplType (Conj f1 f2) == A
fplType (Disj f1 f2) == B
fplType (Impl f1 f2) == B
fplType (Equi f1 f2) == A
fplType (Neg (Conj f1 f2)) == B
fplType (Neg (Disj f1 f2)) == A
fplType (Neg (Impl f1 f2)) == A
fplType (Neg (Equi f1 f2)) == B

It gives the components of a formula for using them in the semantic board

fplComponents f1 == [ Atom "a" ]


fplComponents (Neg f1) == [ Neg (Atom "a") ]


fplComponents (Neg (Neg f1)) == [ Atom "a" ]


fplComponents (Conj f1 f2) == [ Atom "a", Atom "b" ]


fplComponents (Disj f1 f2) == [ Atom "a", Atom "b" ]


fplComponents (Impl f1 f2) == [ Neg (Atom "a"), Atom "b" ]


fplComponents (Equi f1 f2) == [ Impl (Atom "a") (Atom "b"), Impl (Atom "b") (Atom "a") ]


fplComponents (Neg (Conj f1 f2)) == [ Neg (Atom "a"), Neg (Atom "b") ]


fplComponents (Neg (Disj f1 f2)) == [ Neg (Atom "a"), Neg (Atom "b") ]


fplComponents (Neg (Impl f1 f2)) == [ Atom "a", Neg (Atom "b") ]


fplComponents (Neg (Equi f1 f2)) == [ Neg (Impl (Atom "a") (Atom "b")), Neg (Impl (Atom "b") (Atom "a")) ]

It gives if all formulas in a Set of PL formulas are literals.

fs1  = [f1, Neg f2]
fs2 = [f1, Neg f2, Conj f1 f2, Disj f1 f2, Neg (Impl f1 f2), Neg (Equi f1 f2)]
splAllLiterals fs1 == True
splAllLiterals fs2 == False

It removes all Tautological formulas from a set.

It gives if one set of PL formulas contains a formula and its negation or contains the Insat formula (the set is unsatisfiable). If it finds them they return the formulas indices in the set (it is actually a list).

splSearchContradiction fs1 == Nothing
splSearchContradiction fs2 == Nothing


-- If we expand ( Conj f1 f2 ) as [f1, f2] (note that f1 is repeated so we keep only one of its instances)
fs3 = [f1, Neg f2, f2, Disj f1 f2, Neg (Impl f1 f2), Neg (Equi f1 f2)]
splSearchContradiction fs3 == Just [1,2]

It searches a DN formula in the set. If it gets it they return a tuple with the index and the formula, if not Nothing is returned

splSearchDN fs2 == Nothing


-- If we expand Neg(Impl f1 f2) as [(Neg (Neg f1)), (Neg f2)] (note that (Neg f2) is repeated so we keep only one of its instances)
fs4 = [f1, Neg f2, Conj f1 f2, Disj f1 f2, f1, Neg (Equi f1 f2)]
splSearchDN fs4 == Just (4, (Atom "a"))

It searches an Alpha formula in the set. If it gets it they return a tuple with the index and the formula, if not Nothing is returned

splSearchAlpha fs1 == Nothing


splSearchAlpha fs2 == Just ( 2, Conj (Atom "a") (Atom "b") )

It searches an Beta formula in the set. If it gets it they return a tuple with the index and the formula, if not Nothing is returned

splSearchBeta fs1 == Nothing


splSearchBeta fs2 == Just ( 3, Disj (Atom "a") (Atom "b") )

It gives a set of formulas with changing a DN formula by its expansion. If formula is not DN the original set is returned.

splExpandDN fs4 (Neg (Neg f2)) == [ Atom "a", Neg (Atom "b"), Conj (Atom "a") (Atom "b"), Disj (Atom "a") (Atom "b"), Atom "a", Neg (Equi (Atom "a") (Atom "b")), Atom "b" ]

It gives a set of formulas with changing an Alpha formula by its expansion. If formula is not Alpha the original set is returned.

splExpandAlpha fs2 (Conj (Atom "a") (Atom "b")) == [ Atom "a", Neg (Atom "b"), Disj (Atom "a") (Atom "b"), Neg (Impl (Atom "a") (Atom "b")), Neg (Equi (Atom "a") (Atom "b")), Atom "b" ]

It gives a tuple of two sets of formulas with changing a Beta formula by its expansion. If formula is not Beta original set is returned in both sets.

splExpandBeta fs2 (Disj (Atom "a") (Atom "b")) == ( [ Atom "a", Neg (Atom "b"), Conj (Atom "a") (Atom "b"), Neg (Impl (Atom "a") (Atom "b")), Neg (Equi (Atom "a") (Atom "b")) ], [ Atom "a", Neg (Atom "b"), Conj (Atom "a") (Atom "b"), Neg (Impl (Atom "a") (Atom "b")), Neg (Equi (Atom "a") (Atom "b")), Atom "b" ] )

It generates the complete SemanticTableaux as a Graph, which is renderizable with representations methods.

splSemanticTableau fs4 == Graph (Inner { left = Leaf { key = 0, value = { incoming = Empty, node = { id = 0, label = ( 0, [ Atom "a", Neg (Atom "b"), Conj (Atom "a") (Atom "b"), Disj (Atom "a") (Atom "b"), Neg (Equi (Atom "a") (Atom "b")) ] ) }, outgoing = Leaf { key = 1, value = ( A, [ 2 ] ) } } }, prefix = { branchingBit = 1, prefixBits = 0 }, right = Leaf { key = 1, value = { incoming = Leaf { key = 0, value = ( A, [ 2 ] ) }, node = { id = 1, label = ( -1, [ Atom "a", Neg (Atom "b"), Disj (Atom "a") (Atom "b"), Neg (Equi (Atom "a") (Atom "b")), Atom "b" ] ) }, outgoing = Empty } }, size = 2 })

It extracts all the models from a semantic tableau.

splSemanticTableau fs4 |> plSemanticTableauModels == []


fs5 = [Disj f1 f2, Neg(Equi f1 f2)]
splSemanticTableau fs5 |> plSemanticTableauModels == [["a"],["b"]]

It gives the String representation of a tableau.

splSemanticTableau fs4 |> splSemanticTableauToString == "Graph [Node 0 ({a, ¬ b, ( a ∧ b ), ( a ∨ b ), ¬ ( a ↔ b )}), Node 1 ({a, ¬ b, ( a ∨ b ), ¬ ( a ↔ b ), b}), Node 2 (×)] [Edge 1->2 (I (2, 5)), Edge 0->1 (α (3))]"

It gives a String representation of a Tabbleau using DOT notation, which is renderizable with a GraphViz viewer.

splSemanticTableau fs4 |> splSemanticTableauToDOT == "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=box, color=black]\n  edge [dir=none, color=blue, fontcolor=blue]\n\n  0 -> 1 [label=\"α (3)\"]\n  1 -> 2 [label=\"I (2, 5)\"]\n\n  0 [label=\"{a, ¬ b, ( a ∧ b ), ( a ∨ b ), ¬ ( a ↔ b )}\"]\n  1 [label=\"{a, ¬ b, ( a ∨ b ), ¬ ( a ↔ b ), b}\"]\n  2 [label=\"×\"]\n}"