Safe Haskell	None
Language	Haskell98

Data.Logic.ATP.Formulas

Description

The IsFormula class contains definitions for the boolean true and false values, and methods for traversing the atoms of a formula.

Synopsis

Documentation

class (Ord atom, Show atom, HasFixity atom, Pretty atom) => IsAtom atom Source

Basic properties of an atomic formula

Instances

IsAtom Prop Source
IsAtom Atom Source
IsAtom (Knows Integer) Source
(IsPredicate predicate, IsTerm term) => IsAtom (FOLAP predicate term) Source
(IsPredicate predicate, IsTerm term) => IsAtom (FOL predicate term) Source

class (Pretty formula, HasFixity formula, IsAtom (AtomOf formula)) => IsFormula formula where Source

Class associating a formula type with its atom (atomic formula) type.

Associated Types

type AtomOf formula Source

AtomOf is a function that maps the formula type to the associated atomic formula type

Methods

true :: formula Source

The true element

false :: formula Source

The false element

If the arugment is true or false return the corresponding Bool, otherwise return Nothing.

atomic :: AtomOf formula -> formula Source

Build a formula from an atom.

overatoms :: (AtomOf formula -> r -> r) -> formula -> r -> r Source

Formula analog of iterator foldr.

onatoms :: (AtomOf formula -> AtomOf formula) -> formula -> formula Source

Apply a function to the atoms, otherwise keeping structure (new sig)

Instances

IsAtom atom => IsFormula (LFormula atom) Source
IsLiteral a => IsFormula (JL a) Source
IsAtom atom => IsFormula (PFormula atom) Source
(HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsFormula (QFormula v atom) Source

fromBool :: IsFormula formula => Bool -> formula Source

atom_union :: (IsFormula formula, Ord r) => (AtomOf formula -> Set r) -> formula -> Set r Source

Special case of a union of the results of a function over the atoms.