LogicUS.FOL.SyntaxSemantics

The module provides the elementary tools for working with first order logic. It allows defining both formulas and sets as well as performing some basic operations on them, such as evaluations regarding interpretations, performs substitutions, clausures, ...

FOL Formulas and Sets

type alias Ident =

( String, List Int )

It represent an ident as a string and a list of subindices as integers

type alias Variable =

( String, List Int, Int )

It represent a variable as a string, a list of subindices as integers, and a superindex that must be a positive int.

type Term

= Var Variable

| Func Ident (List Term)

It is used to represent the terms in First Order Logic , these are variables, constants and functions. Note that constants are a particular case of functions, which are not dependent on any variable.

type FormulaFOL

= Pred Ident (List Term)

| Equal Term Term

| Neg FormulaFOL

| Conj FormulaFOL FormulaFOL

| Disj FormulaFOL FormulaFOL

| Impl FormulaFOL FormulaFOL

| Equi FormulaFOL FormulaFOL

| Exists Variable FormulaFOL

| Forall Variable FormulaFOL

| Insat

| Taut

It is a recursive definition of a formula in First Order Logic. It could be a predicate, equality, universal cuantification, existencial cuantificacation, negation, conjuction, implication, equivalence and unsatisfiable formula

type alias SetFOL =

List FormulaFOL

It is used to define sets of formulas in First Order Logic.

ffolNegation : FormulaFOL -> FormulaFOL

It gives the negarion of a formula applying idempotent rule or the insat/taut negation when corresponds.

termVarSymbols : Term -> List Variable

It gets all the variable symbols that acts inside a term

termVarSymbols (Func "f" [ Var "a", Func "c" [], Func "g" [ Var "b", Var "a" ] ]) =
    [ "a", "b" ]

termsVarSymbols : List Term -> List Variable

It gets all the variables that acts inside a list of terms

termsVarSymbols [ Func "f" [ Var "a", Func "c" [] ], Func "g" [ Var "b", Var "c" ] ] =
    [ "a", "b", "c" ]

ffolVarSymbols : FormulaFOL -> List Variable

It gets all the variables that acts inside a formula

f1 =
    ffolReadExtraction <| ffolReadFromString "_p(x,y)=_p(y,x)"


f2 =
    ffolReadExtraction <| ffolReadFromString "!A[x] !A[y] (M(x,y) -> !E[z] F(z, _jhon) & P(x,z) | P(y,z))"


ffolVarSymbols f1 =
    [ "x", "y" ]
ffolVarSymbols f2 =
    [ "x", "y", "z" ]

termConstSymbols : Term -> List Ident

It gets all the constant symbols that acts inside a term

termsConstSymbols : List Term -> List Ident

It gets all the constants symbols that acts inside a list of terms

ffolConstSymbols : FormulaFOL -> List Ident

It gets all the constant symbols that acts inside a formula

termFuncSymbols : Term -> List Ident

It gets all the function symbols that acts inside a term

termsFuncSymbols : List Term -> List Ident

It gets all the function symbols that acts inside a list of terms

ffolFuncSymbols : FormulaFOL -> List Ident

It gets all the function symbols that acts inside a formula

ffolPredSymbols : FormulaFOL -> List Ident

It gets all the predicate symbols that acts inside a formula

ffolContainsEquality : FormulaFOL -> Bool

It gets if a formual contains equal predicate or not

ffolFormTree : FormulaFOL -> Graph FormulaFOL ()

It gives a graph with the form tree of a formula. If you want visualize it you can use formTreeToDOT and visualize the result witn an online graphviz render. Don't forget change \\n by \n and \\" by " in a code editor previously.

ffolFormTree f2 |> formTreeToDOT =
    "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=plaintext, color=black]\n  edge [dir=none]\n\n  0 -> 1\n  1 -> 2\n  2 -> 3\n  2 -> 9\n  3 -> 4\n  3 -> 5\n  5 -> 6\n  5 -> 8\n  6 -> 7\n\n  0 [label=\"∀x ∀y ( ( M(x, y) → ( ∃z F(z, jhon) ∧ P(x, z) ) ) ∨ P(y, z) )\"]\n  1 [label=\"∀y ( ( M(x, y) → ( ∃z F(z, jhon) ∧ P(x, z) ) ) ∨ P(y, z) )\"]\n  2 [label=\"( ( M(x, y) → ( ∃z F(z, jhon) ∧ P(x, z) ) ) ∨ P(y, z) )\"]\n  3 [label=\"( M(x, y) → ( ∃z F(z, jhon) ∧ P(x, z) ) )\"]\n  4 [label=\"M(x, y)\"]\n  5 [label=\"( ∃z F(z, jhon) ∧ P(x, z) )\"]\n  6 [label=\"∃z F(z, jhon)\"]\n  7 [label=\"F(z, jhon)\"]\n  8 [label=\"P(x, z)\"]\n  9 [label=\"P(y, z)\"]\n}"

ffolIsWellFormed : FormulaFOL -> Bool

It indicates if a formula is well formed or not. A formula is well formed if it doesn't contain two nested cuantifiers over the same variable

f3 = ffolReadExtraction <| ffolReadFromString "!A[x] !A[y] (M(x,y) -> !E[x] F(x, _jhon) & P(x,x) | P(y,x))"


ffolIsWellFormed f1 == True
ffolIsWellFormed f2 == True
ffolIsWellFormed f3 == False

ffolHasInstanceOfVar : FormulaFOL -> Variable -> Bool

It gives if a formula contains an instance of the variable given.

ffolHasFreeInstanceOfVar : FormulaFOL -> Variable -> Bool

It checks if in one formula if it exists any free instance of a given variable

ffolHasLinkedInstanceOfVar : FormulaFOL -> Variable -> Bool

It checks if in one formula if it exists any linked instance of a given variable

ffolFreeVars : FormulaFOL -> List Variable

It gives the variables of the formulas that are free. That is, variables that have a free instance in the formula

ffolLinkedVars : FormulaFOL -> List Variable

It gives the variables of the formulas that are linked. That is, variables that have a linked instance in the formula

termIsClosed : Term -> Bool

It determinates if a term is closed this is if it doesn't contains any variable

termClosedTerms : Term -> List Term

It gives the all the closed terms inside a term (including the entire term if it is closed)

ffolAllClosedTerms : FormulaFOL -> List Term

It gives the all the closed terms inside a formula

ffolIsOpen : FormulaFOL -> Bool

It determinates if a formula is opened this is if it doesn't contains any cuantifier

ffolIsClosed : FormulaFOL -> Bool

It checks if s formula is closed this is if it hasn't any free variables

Substitutions, variable rename and clausure

type alias Substitution =

Dict Variable Term

It defines a substitution in First Order Logic

substitutionDomain : Substitution -> List Variable

It gets the variable domain of the substitution, that is variables symbols that participates in it.

termApplySubstitution : Substitution -> Term -> Term

It performes a substitution in a term, replacing the variables according to the substitution.

ffolApplySubstitution : Substitution -> FormulaFOL -> FormulaFOL

It performes a substitution in a formula, replacing the variables according to the substitution.

substitutionComposition : Substitution -> Substitution -> Substitution

It gives the composition of two substitutions (s1 ∘ s2)

renameVars : FormulaFOL -> FormulaFOL

It renames variables in a formula if it is necessary. If a instance is linked to several cuantifiers (non well formed formula) it takes the nearest one as reference.

ffolUniversalClausure : FormulaFOL -> FormulaFOL

It gives the universal clausure of a formula

ffolExistencialClausure : FormulaFOL -> FormulaFOL

It gives the existencial clausure of a formula

L-structures and valuations

type alias L_Structure comparable =

( Set comparable

, { const : Dict Ident comparable

, func : Dict Ident ( Int, Dict (List comparable) comparable )

, pred : Dict Ident ( Int, Set (List comparable) )

}

)

It defines an interpretation in First Order Logic, this is a pair of a set of elements (universe) and a record with the following keys and values:

key:const, value: A dictionary that asigns to each constant symbol a element of the universe.
key:func, value: A dictionary that asigns to each function symbol, $f$, a tuple whose first argument regards to the arity, $n$, and second one a dictionary (who emulates a total function) that assigns to each posible k-tuple (as a list) of elements of the universe an element of this universe.
key:pred, value: A dictionary that asigns to each predicate symbol, $P$, a tuple whose first argument regards to the arity, $n$, and second one the set of k-tuples (as lists) of elements of the universe that verifies the predicate.

lStructureIsValid : L_Structure comparable -> Bool

It checks that a L_Structure is valid, that is:

If all the values asigned to the constants are in the universe
For each function symbol, of arity k, all the possible k-tuples (as lists) of elements for the universe must be in the associated dictionary, and all the elements of its range must be in the universe.
For each predicate symbol, all the elements of the associated set must be lists whose length matches with the regarding arity and whose elements belongs to the universe

termInterpretation : Term -> L_Structure comparable -> Maybe comparable

It calculates the interpretation of a closed term regarding to a L_structure. If it is not interpretable by the L_struncture then it returns Nothing.

termsInterpretation : List Term -> L_Structure comparable -> Maybe (List comparable)

It calculates the interpretations of a list of closed terms, if any of them is not interpretable then it returns Nothing.

ffolValuation : FormulaFOL -> L_Structure comparable -> Maybe Bool

It calculates the valuation of a formula regarding to an interpretation. If the formula is not closed or any element is not interpretable it returns Nothing.

sfolInterpretation : SetFOL -> L_Structure comparable -> Maybe Bool

It calculates the valuation of a set of closed formulas regarding to an interpretation. If any formula is interpretable it returns Nothing.

Parsers

ffolReadFromString : String -> ( Maybe FormulaFOL, String, String )

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. The rules of the notation are:

The variables correspond to strings of characters, the first in lowercase, and optionally indexed by natural numbers, which have been written between the symbols _{ and } and separated by commas. For example: x,y_{1}, xA_{1,1}.
The functions are described analogously to the variables but preceding the symbol *. In addition, the arguments, if any, are specified between parentheses and separated by commas. Examples of constants *a,*b_{1},*john, and functions (not constants): *f(x), *g_{1}(x, *a),*father(*john), ...
Predicates are described in a similar way to functions, as strings of characters, the first in uppercase, and followed, if applicable, by a list of terms, specified in parentheses and separated by commas, in the same way as presented for functions. Examples of predicates P,Q_{1}(x),Uncle(*john, *paul), ...
The use of connectives is equivalent proposed for propositional logic, using & for conjunction, | for disjunction, -> for implication, <-> for equivalence and ¬ or - for negation with classical priority(negation, conjunction, disjunction, implication, equivalence) and the use of parentheses to indicate another association priority.
Quantifiers are described as !E for the existential!A for the universal, followed by the variable indicated in brackets, [ and ], and by the quantized formula. As an example, the inductive property on a function (f) can be expressed as: !A[x_{1}] !A[x_{2}](*f(x_{1}) = *f(x_{2}) -> *x_{1} = *f(x_{2})), or the membership of a value (a) to the range of a function (g) like !E[x](*g(x) = *a)).
As in propositional logic, the valid formula is defined by !T and the unsatisfiable formula for!F.
The external parentheses of the formulas should not be put, since the Parser will put them automatically, so their use or not is irrelevant. Error messages are not perfect but we're working to improve it.

ffolReadExtraction : ( Maybe FormulaFOL, String, String ) -> FormulaFOL

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

ffolToInputString : FormulaFOL -> String

It gives the corresponding input syntax of a formula

substitutionReadFromString : String -> ( Maybe Substitution, String, String )

It returns a tuple with may be a substitution (if it can be read it), the input considerated to parse and a message of error if it is not able to performs the parsing. -- Messages are not perfect but we're working to improve it.

substitutionReadExtraction : ( Maybe Substitution, String, String ) -> Substitution

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

substitutionToInputString : Substitution -> String

It generates the corresponding string input of a substitution

Representation

varToString : Variable -> String

It generates the string of a variable

varsToString : List Variable -> String

It generates the string of a list of variables

varToMathString : Variable -> String

It generates the string of a variable using Latex Notation

varsToMathString : List Variable -> String

It generates the string of a list of identifier

identToString : Ident -> String

It generates the string of an identifier

identsToString : List Ident -> String

It generates the string of a list of identifier

identToMathString : Ident -> String

It generates the string of an identifier using Latex notation

identsToMathString : List Ident -> String

It generates the string of a list of identifier

termToString : Term -> String

It generates the string of a term

termsToString : List Term -> String

It generates the string of a list of terms (parameters)

termToMathString : Term -> String

It generates the string of a term using latex notation

termsToMathString : List Term -> String

It generates the string of a list of terms (parameters) using latex notation

ffolToString : FormulaFOL -> String

It generates the string of a First Order Logic Formula,

sfolToString : SetFOL -> String

It generates the string of a First Order Logic Set of formulas,

ffolToMathString : FormulaFOL -> String

It generates the string of a First Order Logic Formula using latex notation

sfolToMathString : SetFOL -> String

It generates the string of a First Order Logic Set of formulas using latex notation as an array

sfolToMathString2 : SetFOL -> String

It generates the string of a First Order Logic Set of formulas using latex notation as an array

formTreeToString : Graph FormulaFOL () -> String

It gives a string representation of a form tree

formTreeToDOT : Graph FormulaFOL () -> String

It gives a string representation of a form tree using DOT format

substitutionToString : Substitution -> String

It gives a string representation of a substitution using latex notation

substitutionToMathString : Substitution -> String

It gives a string representation of a substitution using latex notation

l_StructureToString : L_Structure comparable -> (comparable -> String) -> String

It gives a L-structure as string. It needs a funtion that gives the string representation of the elements of the L-Structure

vicramgon/logicus/10.1.0

LogicUS.FOL.SyntaxSemantics

FOL Formulas and Sets

Substitutions, variable rename and clausure

L-structures and valuations

Parsers

Representation

Modules

Propositional Logic

First Order Logic