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