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

NOTE: the latest version is 5.0.1

Formula

This library exports and parses formulas.

Definitions

type Formula
= Atom String (List Term)
| Neg 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 (List DeadEnd) Formula

Parse string to Formula

parseSigned : String -> Result (List DeadEnd) (Signed Formula)

Parse string to Signed Formula

parseTerm : String -> Result (List DeadEnd) Term

Parses string to Term

Strings

strFormula : Formula -> String

String representation of a Formula

String representation of a Signed Formula

strTerm : Term -> String

String representation of a Term

strSubstitution : Substitution -> String

String representation of a Substitution

errorString : List DeadEnd -> String

Format parsing error

Tableau helpers

substitute : Substitution -> Formula -> Result String Formula

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

Is the signed formula of type Alpha

Is the signed formula of type Beta

Is the signed formula of type Gamma

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

Is the first Signed Formula complementary of the second Signed Formula

Is the first a Signed subformula of the second

Get Formula out of Signed Formula

Get signed subformulas as a list of signed formulas

Is the first a subformula of the second