logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Safe HaskellNone

Data.Logic.Harrison.Equal

Documentation

predicates :: forall formula atom term v p. (FirstOrderFormula formula atom v, AtomEq atom p term, Ord p) => formula -> Set (PredicateName p)Source

function_congruence :: forall fof atom term v p f. (FirstOrderFormula fof atom v, AtomEq atom p term, Term term v f) => (f, Int) -> Set fofSource

predicate_congruence :: (FirstOrderFormula fof atom v, AtomEq atom p term, Term term v f, Ord p) => PredicateName p -> Set fofSource

equivalence_axioms :: forall fof atom term v p f. (FirstOrderFormula fof atom v, AtomEq atom p term, Term term v f, Ord fof) => Set fofSource

equalitize :: forall formula atom term v p f. (FirstOrderFormula formula atom v, Formula formula atom, AtomEq atom p term, Ord p, Show p, Term term v f, Ord formula, Ord f) => formula -> formulaSource

functions' :: forall formula atom f. (Formula formula atom, Ord f) => (atom -> Set (f, Int)) -> formula -> Set (f, Int)Source