Unavailable. Nobody can download this version any more, with elm or with the Lamdera compiler: github.com/vicramgon/logicus is gone (deleted or private); Software Heritage not asked yet (this run's --swh-calls were used up); no fork with tag 6.0.0 found (12 same-name repos checked); no cached copy. Use another version.
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, ...
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
It is used to define sets of formulas in First Order Logic.
It gives the negarion of a formula applying idempotent rule or the insat/taut negation when corresponds.
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" ]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" ]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" ]It gets all the constant symbols that acts inside a term
It gets all the constants symbols that acts inside a list of terms
It gets all the constant symbols that acts inside a formula
It gets all the function symbols that acts inside a term
It gets all the function symbols that acts inside a list of terms
It gets all the function symbols that acts inside a formula
It gets all the predicate symbols that acts inside a formula
It gets if a formual contains equal predicate or not
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}"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 == FalseIt gives if a formula contains an instance of the variable given.
It checks if in one formula if it exists any free instance of a given variable
It checks if in one formula if it exists any linked instance of a given variable
It determinates if a term is closed this is if it doesn't contains any variable
It gives the all the closed terms inside a term (including the entire term if it is closed)
It gives the all the closed terms inside a formula
It determinates if a formula is opened this is if it doesn't contains any cuantifier
It checks if s formula is closed this is if it hasn't any free variables
It defines a substitution in First Order Logic
It gets the variable domain of the substitution, that is variables symbols that participates in it.
It performes a substitution in a term, replacing the variables according to the substitution.
It performes a substitution in a formula, replacing the variables according to the substitution.
It gives the composition of two substitutions (s1 ∘ s2)
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.
It gives the universal clausure of a formula
It gives the existencial clausure of a formula
It defines an interpretation in First Order Logic, this is a pair of a list 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:funct, value: A dictionary that asigns to each function symbol, $f$, a tuple whose first argument regards to the arity, $n$, and second one a function $U^{n} \longrightarrow U$ , that takes a list with $n$ elements of the universe and returns a element of the 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 a predicate $U^{n} \longrightarrow {F, T}$ , that takes a list with $n$ elements of the universe and returns a boolean value.
It calculates the interpretation of a term regarding to a L_structure. If it is not interpretable by the L_struncture then it returns Nothing.
It calculates the interpretations of a list of terms, if any of them is not interpretable then it returns Nothing.
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.
It calculates the valuation of a set of formulas regarding to an interpretation. If any formula is interpretable it returns Nothing.
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.
Messages are not perfect but we're working to improve it.
It extract the formula readed. If it is Nothing it returns Insat
It gives the corresponding input syntax of a formula
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.
It extract the formula readed. If it is Nothing it returns Insat
It generates the corresponding string input of a substitution
It generates the string of a First Order Logic Formula,
It generates the string of a First Order Logic Set of formulas,
It generates the string of a First Order Logic Formula using latex notation
It generates the string of a First Order Logic Set of formulas using latex notation
It gives a string representation of a form tree
It gives a string representation of a form tree using DOT format
It gives a string representation of a substitution using latex notation
It gives a string representation of a substitution using latex notation
It gives a L-structure as string. It needs a funtion that gives the string representation of the elements of the L-Structure
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.