It is used to represent the propositional symbols of the formulas. It is recommended to use lowercase alphabetic characters using "_ {...}" to indicate subscripts.

-- Some examples of propositional symbols
simpleSymbs : List PSymb
simpleSymbs =
    [ "a", "b", "p", "q", "jhon", "marie" ]


subindexedSymb : List PSymb
subindexedSymb =
    [ "a_{1}", "p_{2,3}" ]

It is used to define propositional formulas recursively. It allows defining atoms, negations, conjunctions, disjunctions, implications, equivalences, and unsatisfiable formulas.

-- Some examples of definition of propositional formulas
-- f1 = a → b
f1 =
    Impl (Atom "a") (Atom "b")


-- f2 = ¬(a ∧ b) ↔ (¬a ∨ ¬b)
f2 =
    Equi (Neg (Conj (Atom "a") (Atom "b"))) (Disj (Neg (Atom "a")) (Neg (Atom "b")))

It corresponds to an Atom or a negation of an Atom

It is used to define sets of propositional formulas.

-- fs = {a → b, ¬(a ∧ b) ↔ (¬a ∨ ¬b)}
fs =
    [ f1, f2 ]

It is used to give a sparse definition of an Interpretation as a list of PSymb. This definition assumed that symbols including in the list are considered True. The rest are considered False.

-- i1 = {a=0, b=1}
i1 =
    [ "b" ]


-- i2 ={a=1, b=0}
i2 =
    [ "a" ]


-- i3 = {a=1, b=1}
i3 =
    [ "a", "b" ]

It checks if a formula is a literal or not.

fplIsLiteral (Atom "p\_{1}") == True
fplIsLiteral (Neg(Atom "p\_{1}")) == True
fplIsLiteral (Disj (Atom "p\_{1}") (Atom "p\_{2}")) == False

It checks if a formula is a positive literal or not

fplIsPositiveLiteral (Atom "p\_{1}") == True


fplIsPositiveLiteral (Neg(Atom "p\_{1}")) == False


fplIsPositiveLiteral (Disj (Atom "p\_{1}") (Atom "p\_{2}")) == False

It checks if a formula is a negative literal or not

fplIsNegativeLiteral (Atom "p\_{1}") == False


fplIsNegativeLiteral (Neg(Atom "p\_{1}")) == True


fplIsNegativeLiteral (Disj (Atom "p\_{1}") (Atom "p\_{2}")) == False

It gives the negation of a formula.

fplNegation (Neg f1) == f1


fplNegation Insat == Insat


fplNegation f1 = Neg f1

It calculates all the symbols that take place in a formula

fplSymbols f1 == [ "a", "b" ]


fplSymbols f2 == [ "a", "b" ]

It gives a Graph.Graph with the form tree of a formula. If you want visualize it you can use formTreeHTML (defined in module Logicus.Base.Repr.SintaxSemantics.HTML) that gives a dot code of the graph. You can visualize it in a online graphviz visualizer or you can create an html file and follow the instructions (defined in Logicus.PL.Repr.Common.GraphViz).

fplFormTree f1 == Graph.Graph (Inner { left = Inner { left = Leaf { key = 0, value = { incoming = Empty, node = { id = 0, label = Impl (Atom "a") (Atom "b") }, outgoing = Inner { left = Leaf { key = 1, value = () }, prefix = { branchingBit = 2, prefixBits = 0 }, right = Leaf { key = 2, value = () }, size = 2 } } }, prefix = { branchingBit = 1, prefixBits = 0 }, right = Leaf { key = 1, value = { incoming = Leaf { key = 0, value = () }, node = { id = 1, label = Atom "a" }, outgoing = Empty } }, size = 2 }, prefix = { branchingBit = 2, prefixBits = 0 }, right = Leaf { key = 2, value = { incoming = Leaf { key = 0, value = () }, node = { id = 2, label = Atom "b" }, outgoing = Empty } }, size = 3 })

It calculates the truth value of a formula regarding to an interpretation.

fplValuation f1 i1 == True


fplValuation f1 i2 == False


fplValuation f2 i3 == True

It gives all possible interpretations of a formula.

fplInterpretations f1 == [ [], [ "b" ], [ "a" ], [ "a", "b" ] ]


fplInterpretations f2 == [ [], [ "b" ], [ "a" ], [ "a", "b" ] ]

It gives all models of a formula

fplModels f1 == [ [], [ "b" ], [ "a", "b" ] ]


fplModels f2 == [ [], [ "b" ], [ "a" ], [ "a", "b" ] ]

It gives all countermodels of a formula

fplCountermodels f1 == [ [ "a" ] ]


fplCountermodels f2 == []

It gives all models and countermodels of a formula as a tuple (models, countermodels).

fplModelsCountermodels f1 == ( [ [], [ "b" ], [ "a", "b" ] ], [ [ "a" ] ] )


fplModelsCountermodels f2 == ( [ [], [ "b" ], [ "a" ], [ "a", "b" ] ], [] )

It gives the truth table of a formula as a List(Interpretation, Bool). You cab visualize it as a table using the function fplTruthTableHTML (defined in module Logicus.Base.Repr.SintaxSemantics.HTML) or using fplTruthTableMathString (defined in module Logicus.Base.Repr.SintaxSemantics.Latex) and follow the instructions given in the respective module.

fplTruthTable f1 == [ ( [], True ), ( [ "b" ], True ), ( [ "a" ], False ), ( [ "a", "b" ], True ) ]


flpTruthTable f2 == [ ( [], True ), ( [ "b" ], True ), ( [ "a" ], True ), ( [ "a", "b" ], True ) ]

It gives if a formula is satisfiable (bruteforce)

fplSatisfiability f1 == True


fplSatisfiability f2 == True

It gives if a formula is a tautology (bruteforce)

fplValidity f1 == False


fplValidity f2 == True

It calculates all the symbols that take place in a set of formulas

fplSymbols f2 == [ "a", "b" ]

It calculates the truth value of a set of formulas regarding to an interpretation.

splValuation fs i1 == True


splValuation fs i2 == False


splValuation fs i3 == True

It gives all possible interpretations of a set of formulas.

splInterpretations fs == [ [], [ "b" ], [ "a" ], [ "a", "b" ] ]

It gives all models of a set of formulas

splModels fs == [ [], [ "b" ], [ "a", "b" ] ]

It gives all countermodels of a set of formulas

splCountermodels fs == [ [ "a" ] ]

It gives all models and countermodels of a set of formulas as a tuple (models, countermodels).

splModelsCountermodels fs == ( [ [], [ "b" ], [ "a", "b" ] ], [ [ "a" ] ] )

It gives the truth table of a set of formulas as a List(Interpretation, Bool). You can visualize it as a table using the function splTruthTableHTML (defined in module Logicus.Base.Repr.SintaxSemantics.HTML) or using splTruthTableLatex (defined in module Logicus.Base.Repr.SintaxSemantics.Latex) and follow the instructions given in the respective module.

splTruthTable fs == [ ( [], True ), ( [ "b" ], True ), ( [ "a" ], False ), ( [ "a", "b" ], True ) ]

It gives if a set of formulas is satisfiable (bruteforce)

splSatisfiability fs == True


splSatisfiability (fs ++ [ Atom "a", Neg (Atom "b") ]) == False

It gives if a set of formulas is unsatisfiable (bruteforce)

splUnsatisfiability fs == False


splUnatisfiability (fs ++ [ Atom "a", Neg (Atom "b") ]) == True

It gives if a if a formula F is consecuence of a set of formulas S checking if all model of S is also model of F. (bruteforce)

logicalConsecuence fs (Disj (Neg (Atom "a")) (Atom "b")) == True


logicalConsecuence fs Insat == False


logicalConsecuence [ Insat ] f1 == True -- You can deduce anything of an unsatifiable set.

It gives if a if a formula F is consecuence of a set of formulas S checking if S U {F} is unsatisfiable. (bruteforce)

logicalConsecuence2 fs (Disj (Neg (Atom "a")) (Atom "b")) == True


logicalConsecuence2 fs Insat == False


logicalConsecuence2 [ Insat ] f1 == True -- You can deduce anything of an unsatifiable set.

It reads the formula from a string. It returns a tuple with may be a formula (if it can be read it), the input considerated to parse and a message of error it it is not able to performs the parsing.

fplReadFromString "p" == ( Just (Atom "p"), "p", "" )


fplReadFromString "p_{1} /\\ p_{2}" == ( Just (Conj (Atom "p_{1}") (Atom "p_{2}")), "(p_{1}/\\p_{2})", "" )


fplReadFromString "(p \\/ q -> r)" == ( Just (Impl (Disj (Atom "p") (Atom "q")) (Atom "r")), "((p\\/q)->r)", "" )


fplReadFromString "p_{1,1} <-> p_{1,2}" == ( Just (Equi (Atom "p_{1,1}") (Atom "p_{1,2}")), "(p_{1,1}<->p_{1,2})", "" )


fplReadFromString "_|_" == ( Just Insat, "_|_", "" )


fplReadFromString "p_1" == ( Nothing, "(p_1)", "Error: [{ col = 3, problem = ExpectingSymbol ')', row = 1 }]" )

Messages are not perfect but we're working to improve it.

It extract the formula readed. If it is Nothing it returns Insat

f3 = fplReadExtraction <| fplReadFromString "(p \\/ q -> r)"
f3 == Impl (Disj (Atom "p") (Atom "q")) (Atom "r")
f4 = fplReadExtraction <| fplReadFromString "(p \\/ q <- r)"
f4 == Insat

It gives the corresponding input syntax of a formula

fplToInputString f3 == "((p\\/q)->r)"


fplToInputString f4 == "_|_"

It generates the String representation of a PL formula using unicode symbols.

fplToString f1 == "( a → b )"


fplToString f2 == "( ¬ ( a ∧ b ) ↔ ( ¬ a ∨ ¬ b ) )"

It generates the Latex string of a PL formula. The result requires a math enviroment to be displayed.

fplToMathString f1 == "\\left( a\\rightarrow b \\right)"


fplToMathString f2 == "\\left( \\neg \\left( a \\wedge b \\right)\\leftrightarrow \\left( \\neg a \\vee \\neg b \\right) \\right)"

It generates the Truth Table of a PL formula as a string using CSV format (separated by ';')

fplTruthTableString f1 == ""a ; b ; ( a → b ) \nF ; F ; T \nF ; T ; T \nT ; F ; F \nT ; T ; T""
fplTruthTableString f2 == "a ; b ; ( ¬ ( a ∧ b ) ↔ ( ¬ a ∨ ¬ b ) ) \nF ; F ; T \nF ; T ; T \nT ; F ; T \nT ; T ; T"

It generates the Latex code of a Truth Table of a PL formula. The result requires a math enviroment to be displayed.

fplTruthTableMathString f1 == "\\begin{array}{c|c|c|}\n\mathbf{a} & \\mathbf{b} & \\mathbf{\\left( a\\rightarrow b \\right)} \\\\ \\hline \nF & F & T \\\\ \nF & T & T \\\\ \nT & F & F \\\\ \nT & T & T \\\\ \\end{array}"


fplTruthTableMathString f2 == "\\begin{array}{c|c|c|}\n\n\\mathbf{a} & \\mathbf{b} & \\mathbf{\\left( \\neg \\left( a \\wedge b \\right)\\leftrightarrow \\left( \\neg a \\vee \\neg b \\right) \\right)} \\\\\\hlineF & F & T \\\\ \nF & T & T \\\\ \nT & F & T \\\\ \nT & T & T \\\\ \\end{array}"

It gives the String representation of a formTree.

fplFormTreeToString <| fplFormTree f3 == "0 ( ( p ∨ q ) → r )\n1 ( p ∨ q )\n2 p\n3 q\n4 r\n#\n0 1\n0 4\n1 2\n1 3"

It generates the formation tree of a formula as DOT string. It requires a GraphViz interpreter to be displayed.

fplFormTreeToDOT <| fplFormTree f3 == "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=plaintext, color=black]\n  edge [dir=none]\n\n  0 -> 1\n  0 -> 4\n  1 -> 2\n  1 -> 3\n\n  0 [label=\"( ( p ∨ q ) → r )\"]\n  1 [label=\"( p ∨ q )\"]\n  2 [label=\"p\"]\n  3 [label=\"q\"]\n  4 [label=\"r\"]\n}"

It generates the String of Set of PL formulas using unicode symbols.

splToString [ f1, f2 ] == "{( a → b ), ( ¬ ( a ∧ b ) ↔ ( ¬ a ∨ ¬ b ) )}"

It generates the Latex string of a Set of PL formulas. The result requires a math enviroment to be displayed.

splToMathString [ f1, f2 ] == "\\left\\lbrace \\left( a\\rightarrow b \\right), \\left( \\neg \\left( a \\wedge b \\right)\\leftrightarrow \\left( \\neg a \\vee \\neg b \\right) \\right)\\right\\rbrace"

It generates the Truth Table of a set of PL formulas as a string using CSV format.

splTruthTableString [ f1, f2 ] == "a ; b ; ( a → b ) ; ( ¬ ( a ∧ b ) ↔ ( ¬ a ∨ ¬ b ) ) ; U \n0 ; 0 ; T ; T ; T \n0 ; 1 ; T ; T ; T \n1 ; 0 ; F ; T ; F \n1 ; 1 ; T ; T ; T"

It generates the Latex code of a Truth Table of Set of PL formulas. The result requires a math enviroment to be displayed.

splTruthTableMathString [ f1, f2 ] =
    "\\begin{array}{c|c|c|c|c|}\\mathbf{a} & \\mathbf{b} & \\mathbf{\\left( a\\rightarrow b \\right)} & \\mathbf{\\left( \\neg \\left( a \\wedge b \\right)\\leftrightarrow \\left( \\neg a \\vee \\neg b \\right) \\right)} & \\mathbf{U} \\\\ \\hlineF & F & T & T & T \\\\ F & T & T & T & T \\\\ T & F & F & T & F \\\\ T & T & T & T & T \\\\ \\end{array}"

It calculates the list of interpretations from a list of symbols and a list of literals taking each symbol as true if it apears as positive literal, as negative if it apears as negative literal and indiferent if it doesn't appear.