Formula

This library exports formulas.

Definitions

= PredAtom String (List Term)

| EqAtom Term Term

| Neg Formula

| ForAll String Formula

| Exists String Formula

| FF

| FT

Formula

String representation of a Formula

substitute : Substitution -> Formula -> Result String Formula

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

free : Formula -> Set String

Returns set of all free variables in given formula

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

Is the first a subformula of the second