Data.Logic.Classes.FirstOrder

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 where

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.

Methods

for_all :: v -> formula -> formula

Universal quantification - for all x (formula x)

exists :: v -> formula -> formula

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

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

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.

Instances

(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

data Quant

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.

Constructors

Forall

Exists

Instances

Bounded Quant

Enum Quant

Eq Quant

Data Quant

Ord Quant

Read Quant

Show Quant

Typeable Quant

SafeCopy 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

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 -> 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

for_all with a list of variables, for backwards compatibility.

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

exists with a list of variables, for backwards compatibility.

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

Helper function for building folds.

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

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

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

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

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

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

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

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 -> formula2

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

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 -> r

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 -> String

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 -> 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

Deprecated - use mapAtoms

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

Deprecated - use foldAtoms

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

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 -> fof