Safe Haskell | None |
---|

- class (Formula formula atom, Combinable formula, Constants formula, Constants atom, HasFixity atom, Variable v, Pretty atom, Pretty v) => FirstOrderFormula formula atom v | formula -> atom v where
- for_all :: v -> formula -> formula
- exists :: v -> formula -> formula
- foldFirstOrder :: (Quant -> v -> formula -> r) -> (Combination formula -> r) -> (Bool -> r) -> (atom -> r) -> formula -> r

- data Quant
- zipFirstOrder :: FirstOrderFormula formula atom v => (Quant -> v -> formula -> Quant -> v -> formula -> Maybe r) -> (Combination formula -> Combination formula -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (atom -> atom -> Maybe r) -> formula -> formula -> Maybe r
- pApp :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> [term] -> formula
- pApp0 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> formula
- pApp1 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> formula
- pApp2 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> formula
- pApp3 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> formula
- pApp4 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> formula
- pApp5 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> formula
- pApp6 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> formula
- pApp7 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula
- for_all' :: FirstOrderFormula formula atom v => [v] -> formula -> formula
- exists' :: FirstOrderFormula formula atom v => [v] -> formula -> formula
- quant :: FirstOrderFormula formula atom v => Quant -> v -> formula -> formula
- (!) :: FirstOrderFormula formula atom v => v -> formula -> formula
- (?) :: FirstOrderFormula formula atom v => v -> formula -> formula
- (∀) :: FirstOrderFormula formula atom v => v -> formula -> formula
- (∃) :: FirstOrderFormula formula atom v => v -> formula -> formula
- quant' :: FirstOrderFormula formula atom v => Quant -> [v] -> formula -> formula
- convertFOF :: (FirstOrderFormula formula1 atom1 v1, FirstOrderFormula formula2 atom2 v2) => (atom1 -> atom2) -> (v1 -> v2) -> formula1 -> formula2
- toPropositional :: forall formula1 atom v formula2 atom2. (FirstOrderFormula formula1 atom v, PropositionalFormula formula2 atom2) => (atom -> atom2) -> formula1 -> formula2
- withUnivQuants :: FirstOrderFormula formula atom v => ([v] -> formula -> r) -> formula -> r
- showFirstOrder :: forall formula atom v. (FirstOrderFormula formula atom v, Show v) => (atom -> String) -> formula -> String
- prettyFirstOrder :: forall formula atom v. FirstOrderFormula formula atom v => (Int -> atom -> Doc) -> (v -> Doc) -> Int -> formula -> Doc
- fixityFirstOrder :: (HasFixity atom, FirstOrderFormula formula atom v) => formula -> Fixity
- foldAtomsFirstOrder :: FirstOrderFormula fof atom v => (r -> atom -> r) -> r -> fof -> r
- mapAtomsFirstOrder :: forall formula atom v. FirstOrderFormula formula atom v => (atom -> formula) -> formula -> formula
- onatoms :: forall formula atom v. FirstOrderFormula formula atom v => (atom -> formula) -> formula -> formula
- overatoms :: forall formula atom v r. FirstOrderFormula formula atom v => (atom -> r -> r) -> formula -> r -> r
- atom_union :: forall formula atom v a. (FirstOrderFormula formula atom v, Ord a) => (atom -> Set a) -> formula -> Set a
- fromFirstOrder :: forall formula atom v lit atom2. (Formula lit atom2, FirstOrderFormula formula atom v, Literal lit atom2) => (atom -> atom2) -> formula -> Failing lit
- fromLiteral :: forall lit atom v fof atom2. (Literal lit atom, FirstOrderFormula fof atom2 v) => (atom -> atom2) -> lit -> fof

# Documentation

class (Formula formula atom, Combinable formula, Constants formula, Constants atom, HasFixity atom, Variable v, Pretty atom, Pretty v) => FirstOrderFormula formula atom v | formula -> atom v whereSource

The `FirstOrderFormula`

type class. Minimal implementation:
`for_all, exists, foldFirstOrder, foldTerm, (.=.), pApp0-pApp7, fApp, var`

. The
functional dependencies are necessary here so we can write
functions that don't fix all of the type parameters. For example,
without them the univquant_free_vars function gives the error ```
No
instance for (FirstOrderFormula Formula atom V)
```

because the
function doesn't mention the Term type.

for_all :: v -> formula -> formulaSource

Universal quantification - for all x (formula x)

exists :: v -> formula -> formulaSource

Existential quantification - there exists x such that (formula x)

foldFirstOrder :: (Quant -> v -> formula -> r) -> (Combination formula -> r) -> (Bool -> r) -> (atom -> r) -> formula -> rSource

A fold function similar to the one in `PropositionalFormula`

but extended to cover both the existing formula types and the
ones introduced here. `foldFirstOrder (.~.) quant binOp infixPred pApp`

is a no op. The argument order is taken from Logic-TPTP.

(Formula (Formula a) a, Constants a, Pretty a, HasFixity a) => FirstOrderFormula (Formula a) a String | |

(Formula (Formula v p f) (Predicate p (PTerm v f)), AtomEq (Predicate p (PTerm v f)) p (PTerm v f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v | |

(Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v | |

(Formula (NormalSentence v p f) (NormalSentence v p f), Combinable (NormalSentence v p f), Term (NormalTerm v f) v f, Variable v, Predicate p, Function f v) => FirstOrderFormula (NormalSentence v p f) (NormalSentence v p f) v | |

(Formula (Sentence v p f) (Sentence v p f), Variable v, Predicate p, Function f v) => FirstOrderFormula (Sentence v p f) (Sentence v p f) v |

The `Quant`

and `InfixPred`

types, like the BinOp type in
`Propositional`

, could be additional parameters to the type
class, but it would add additional complexity with unclear
benefits.

zipFirstOrder :: FirstOrderFormula formula atom v => (Quant -> v -> formula -> Quant -> v -> formula -> Maybe r) -> (Combination formula -> Combination formula -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (atom -> atom -> Maybe r) -> formula -> formula -> Maybe rSource

pApp :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> [term] -> formulaSource

pApp0 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> formulaSource

Versions of pApp specialized for different argument counts.

pApp1 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> formulaSource

pApp2 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> formulaSource

pApp3 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> formulaSource

pApp4 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> formulaSource

pApp5 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> formulaSource

pApp6 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> formulaSource

pApp7 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formulaSource

for_all' :: FirstOrderFormula formula atom v => [v] -> formula -> formulaSource

for_all with a list of variables, for backwards compatibility.

exists' :: FirstOrderFormula formula atom v => [v] -> formula -> formulaSource

exists with a list of variables, for backwards compatibility.

quant :: FirstOrderFormula formula atom v => Quant -> v -> formula -> formulaSource

Helper function for building folds.

(!) :: FirstOrderFormula formula atom v => v -> formula -> formulaSource

Names for for_all and exists inspired by the conventions of the TPTP project.

(?) :: FirstOrderFormula formula atom v => v -> formula -> formulaSource

(∀) :: FirstOrderFormula formula atom v => v -> formula -> formulaSource

∀ can't be a function when -XUnicodeSyntax is enabled.

(∃) :: FirstOrderFormula formula atom v => v -> formula -> formulaSource

quant' :: FirstOrderFormula formula atom v => Quant -> [v] -> formula -> formulaSource

Legacy version of quant from when we supported lists of quantified variables. It also has the virtue of eliding quantifications with empty variable lists (by calling for_all' and exists'.)

convertFOF :: (FirstOrderFormula formula1 atom1 v1, FirstOrderFormula formula2 atom2 v2) => (atom1 -> atom2) -> (v1 -> v2) -> formula1 -> formula2Source

toPropositional :: forall formula1 atom v formula2 atom2. (FirstOrderFormula formula1 atom v, PropositionalFormula formula2 atom2) => (atom -> atom2) -> formula1 -> formula2Source

Try to convert a first order logic formula to propositional. This will return Nothing if there are any quantifiers, or if it runs into an atom that it is unable to convert.

withUnivQuants :: FirstOrderFormula formula atom v => ([v] -> formula -> r) -> formula -> rSource

Examine the formula to find the list of outermost universally quantified variables, and call a function with that list and the formula after the quantifiers are removed.

showFirstOrder :: forall formula atom v. (FirstOrderFormula formula atom v, Show v) => (atom -> String) -> formula -> StringSource

Display a formula in a format that can be read into the interpreter.

prettyFirstOrder :: forall formula atom v. FirstOrderFormula formula atom v => (Int -> atom -> Doc) -> (v -> Doc) -> Int -> formula -> DocSource

fixityFirstOrder :: (HasFixity atom, FirstOrderFormula formula atom v) => formula -> FixitySource

foldAtomsFirstOrder :: FirstOrderFormula fof atom v => (r -> atom -> r) -> r -> fof -> rSource

mapAtomsFirstOrder :: forall formula atom v. FirstOrderFormula formula atom v => (atom -> formula) -> formula -> formulaSource

onatoms :: forall formula atom v. FirstOrderFormula formula atom v => (atom -> formula) -> formula -> formulaSource

Deprecated - use mapAtoms

overatoms :: forall formula atom v r. FirstOrderFormula formula atom v => (atom -> r -> r) -> formula -> r -> rSource

Deprecated - use foldAtoms

atom_union :: forall formula atom v a. (FirstOrderFormula formula atom v, Ord a) => (atom -> Set a) -> formula -> Set aSource

fromFirstOrder :: forall formula atom v lit atom2. (Formula lit atom2, FirstOrderFormula formula atom v, Literal lit atom2) => (atom -> atom2) -> formula -> Failing litSource

Just like Logic.FirstOrder.convertFOF except it rejects anything with a construct unsupported in a normal logic formula, i.e. quantifiers and formula combinators other than negation.

fromLiteral :: forall lit atom v fof atom2. (Literal lit atom, FirstOrderFormula fof atom2 v) => (atom -> atom2) -> lit -> fofSource