FMFI-UK-1-AIN-412/elm-formula/1.0.0

NOTE: this package is not compatible with Elm 0.19.1

Formula

This library parses and exports formulas.

Definitions

type Formula
= Atom String (List Term)
| Neg Formula
| Disj Formula Formula
| Conj Formula Formula
| Impl Formula Formula
| ForAll String Formula
| Exists String Formula
| FF
| FT

Formula

type Signed a
= T a
| F a

Signed with T[rue] or F[alse]

type alias Substitution =
Dict String Term

Type alias for substitution

type Term
= Var String
| Fun String (List Term)

Term

Parsers

parse : String -> Result Error Formula

Parse string to Formula

parseSigned : String -> Result Error (Signed Formula)

Parse string to Signed Formula

parseTerm : String -> Result Error Term

Parses string to Term

Strings

strFormula : Formula -> String

String representation of a Formula

strSigned : Signed Formula -> String

String representation of a Signed Formula

strTerm : Term -> String

String representation of a Term

strSubstitution : Substitution -> String

String representation of a Substitution

errorString : Error -> String

Format parsing error

Helpers

substitute : Substitution -> Formula -> Result String Formula

Checks if substitution is applicable and substitutes if yes. Returns Result. ErrMessage or Formula after substitution

isAlpha : Signed Formula -> Bool

Is the signed formula of type Alpha

isBeta : Signed Formula -> Bool

Is the signed formula of type Beta

isGamma : Signed Formula -> Bool

Is the signed formula of type Gamma

isDelta : Signed Formula -> Bool

Is the signed formula of type Delta

freeFormula : Formula -> Set String

Returns set of all free variables in given formula

removeQuantifierAndSubstitute : Substitution -> Formula -> Result String Formula

Removes quantifier from given signed formula and returns formula after substitution or error

isSignedComplementary : Signed Formula -> Signed Formula -> Bool

Is the first Signed Formula complementary of the second Signed Formula

isSignedSubformulaOf : Signed Formula -> Signed Formula -> Bool

Is the first a Signed subformula of the second

signedGetFormula : Signed Formula -> Formula

Get Formula out of Signed Formula

signedSubformulas : Signed Formula -> List (Signed Formula)

Get signed subformulas as a list of signed formulas

isSubformulaOf : Formula -> Formula -> Bool

Is the first a subformula of the second