-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Framework for propositional and first order logic, theorem proving
--   
@package logic-classes
@version 1.5.2


-- | This library provides a representation of boolean formulas that is
--   used by the solver in <a>Data.Boolean.SatSolver</a>.
--   
--   We also define a function to simplify formulas, a type for conjunctive
--   normalforms, and a function that creates them from boolean formulas.
module Data.Boolean

-- | Boolean formulas are represented as values of type <tt>Boolean</tt>.
data Boolean

-- | Variables are labeled with an <tt>Int</tt>,
Var :: Int -> Boolean

-- | <tt>Yes</tt> represents <i>true</i>,
Yes :: Boolean

-- | <tt>No</tt> represents <i>false</i>,
No :: Boolean

-- | <tt>Not</tt> constructs negated formulas,
Not :: Boolean -> Boolean

-- | and finally we provide conjunction
(:&&:) :: Boolean -> Boolean -> Boolean

-- | and disjunction of boolean formulas.
(:||:) :: Boolean -> Boolean -> Boolean

-- | Literals are variables that occur either positively or negatively.
data Literal
Pos :: Int -> Literal
Neg :: Int -> Literal

-- | This function returns the name of the variable in a literal.
literalVar :: Literal -> Int

-- | This function negates a literal.
invLiteral :: Literal -> Literal

-- | This predicate checks whether the given literal is positive.
isPositiveLiteral :: Literal -> Bool

-- | Conjunctive normalforms are lists of lists of literals.
type CNF = [Clause]
type Clause = [Literal]

-- | We convert boolean formulas to conjunctive normal form by pushing
--   negations down to variables and repeatedly applying the distributive
--   laws.
booleanToCNF :: Boolean -> CNF
instance Show Boolean
instance Eq Literal
instance Show Literal


-- | This Haskell library provides an implementation of the
--   Davis-Putnam-Logemann-Loveland algorithm (cf.
--   <a>http://en.wikipedia.org/wiki/DPLL_algorithm</a>) for the boolean
--   satisfiability problem. It not only allows to solve boolean formulas
--   in one go but also to add constraints and query bindings of variables
--   incrementally.
--   
--   The implementation is not sophisticated at all but uses the basic DPLL
--   algorithm with unit propagation.
module Data.Boolean.SatSolver

-- | Boolean formulas are represented as values of type <tt>Boolean</tt>.
data Boolean

-- | Variables are labeled with an <tt>Int</tt>,
Var :: Int -> Boolean

-- | <tt>Yes</tt> represents <i>true</i>,
Yes :: Boolean

-- | <tt>No</tt> represents <i>false</i>,
No :: Boolean

-- | <tt>Not</tt> constructs negated formulas,
Not :: Boolean -> Boolean

-- | and finally we provide conjunction
(:&&:) :: Boolean -> Boolean -> Boolean

-- | and disjunction of boolean formulas.
(:||:) :: Boolean -> Boolean -> Boolean

-- | A <tt>SatSolver</tt> can be used to solve boolean formulas.
data SatSolver

-- | Literals are variables that occur either positively or negatively.
data Literal
Pos :: Int -> Literal
Neg :: Int -> Literal

-- | This function returns the name of the variable in a literal.
literalVar :: Literal -> Int

-- | This function negates a literal.
invLiteral :: Literal -> Literal

-- | This predicate checks whether the given literal is positive.
isPositiveLiteral :: Literal -> Bool

-- | Conjunctive normalforms are lists of lists of literals.
type CNF = [Clause]
type Clause = [Literal]

-- | We convert boolean formulas to conjunctive normal form by pushing
--   negations down to variables and repeatedly applying the distributive
--   laws.
booleanToCNF :: Boolean -> CNF

-- | A new SAT solver without stored constraints.
newSatSolver :: SatSolver

-- | This predicate tells whether all constraints are solved.
isSolved :: SatSolver -> Bool

-- | We can lookup the binding of a variable according to the currently
--   stored constraints. If the variable is unbound, the result is
--   <tt>Nothing</tt>.
lookupVar :: Int -> SatSolver -> Maybe Bool

-- | We can assert boolean formulas to update a <tt>SatSolver</tt>. The
--   assertion may fail if the resulting constraints are unsatisfiable.
assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolver
assertTrue' :: MonadPlus m => CNF -> SatSolver -> m SatSolver

-- | This function guesses a value for the given variable, if it is
--   currently unbound. As this is a non-deterministic operation, the
--   resulting solvers are returned in an instance of <tt>MonadPlus</tt>.
branchOnVar :: MonadPlus m => Int -> SatSolver -> m SatSolver

-- | We select a variable from the shortest clause hoping to produce a unit
--   clause.
selectBranchVar :: SatSolver -> Int

-- | This function guesses values for variables such that the stored
--   constraints are satisfied. The result may be non-deterministic and is,
--   hence, returned in an instance of <tt>MonadPlus</tt>.
solve :: MonadPlus m => SatSolver -> m SatSolver

-- | This predicate tells whether the stored constraints are solvable. Use
--   with care! This might be an inefficient operation. It tries to find a
--   solution using backtracking and returns <tt>True</tt> if and only if
--   that fails.
isSolvable :: SatSolver -> Bool
instance Show SatSolver

module Data.Logic.Failing

-- | An error idiom. Rather like the error monad, but collect all | errors
--   together
data Failing a :: * -> *
Success :: a -> Failing a
Failure :: [ErrorMsg] -> Failing a
failing :: ([String] -> b) -> (a -> b) -> Failing a -> b
instance Ord a => Ord (Failing a)
instance Eq a => Eq (Failing a)
instance Read a => Read (Failing a)
instance Data a => Data (Failing a)
instance Typeable Failing
instance Monad Failing

module Data.Logic.Harrison.Lib
tests :: Test
setAny :: Ord a => (a -> Bool) -> Set a -> Bool
setAll :: Ord a => (a -> Bool) -> Set a -> Bool
tryfind :: (t -> Failing a) -> [t] -> Failing a
settryfind :: (t -> Failing a) -> Set t -> Failing a
(|=>) :: Ord k => k -> a -> Map k a
(|->) :: Ord k => k -> a -> Map k a -> Map k a
fpf :: Ord a => Map a b -> a -> Maybe b
defined :: Ord t => Map t a -> t -> Bool
apply :: Ord k => Map k a -> k -> Maybe a
exists :: (a -> Bool) -> [a] -> Bool
tryApplyD :: Ord k => Map k a -> k -> a -> a
allpairs :: Ord c => (a -> b -> c) -> Set a -> Set b -> Set c
distrib' :: Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
image :: (Ord b, Ord a) => (a -> b) -> Set a -> Set b
optimize :: (b -> b -> Bool) -> (a -> b) -> [a] -> Maybe a
minimize :: Ord b => (a -> b) -> [a] -> Maybe a
maximize :: Ord b => (a -> b) -> [a] -> Maybe a
optimize' :: (b -> b -> Bool) -> (a -> b) -> Set a -> Maybe a
minimize' :: Ord b => (a -> b) -> Set a -> Maybe a
maximize' :: Ord b => (a -> b) -> Set a -> Maybe a
can :: (t -> Failing a) -> t -> Bool
allsets :: (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsubsets :: Ord a => Set a -> Set (Set a)
allnonemptysubsets :: Ord a => Set a -> Set (Set a)
mapfilter :: (a -> Failing b) -> [a] -> [b]
setmapfilter :: Ord b => (a -> Failing b) -> Set a -> Set b
(∅) :: Set a

module Data.Logic.Classes.Negate

-- | The class of formulas that can be negated. There are some types that
--   can be negated but do not support the other Boolean Logic operators,
--   such as the <tt>Literal</tt> class.
class Negatable formula
negatePrivate :: Negatable formula => formula -> formula
foldNegation :: Negatable formula => (formula -> r) -> (formula -> r) -> formula -> r

-- | Is this formula negated at the top level?
negated :: Negatable formula => formula -> Bool

-- | Negate the formula, avoiding double negation
(.~.) :: Negatable formula => formula -> formula
(¬) :: Negatable formula => formula -> formula
negative :: Negatable formula => formula -> Bool
positive :: Negatable formula => formula -> Bool

module Data.Logic.Classes.ClauseNormalForm

-- | A class to represent formulas in CNF, which is the conjunction of a
--   set of disjuncted literals each which may or may not be negated.
class (Negatable lit, Eq lit, Ord lit) => ClauseNormalFormula cnf lit | cnf -> lit
clauses :: ClauseNormalFormula cnf lit => cnf -> Set (Set lit)
makeCNF :: ClauseNormalFormula cnf lit => Set (Set lit) -> cnf
satisfiable :: (ClauseNormalFormula cnf lit, MonadPlus m) => cnf -> m Bool


-- | Substitution and finding variables are two basic operations on
--   formulas that contain terms and variables. If a formula type supports
--   quantifiers we can also find free variables, otherwise all variables
--   are considered free.
module Data.Logic.Classes.Atom
class Atom atom term v | atom -> term v
substitute :: Atom atom term v => Map v term -> atom -> atom
allVariables :: Atom atom term v => atom -> Set v
freeVariables :: Atom atom term v => atom -> Set v
unify :: Atom atom term v => Map v term -> atom -> atom -> Failing (Map v term)
match :: Atom atom term v => Map v term -> atom -> atom -> Failing (Map v term)
foldTerms :: Atom atom term v => (term -> r -> r) -> r -> atom -> r
isRename :: Atom atom term v => atom -> atom -> Bool
getSubst :: Atom atom term v => Map v term -> atom -> Map v term

module Data.Logic.Classes.Pretty

-- | The intent of this class is to be similar to Show, but only one way,
--   with no corresponding Read class. It doesn't really belong here in
--   logic-classes. To put something in a pretty printing class implies
--   that there is only one way to pretty print it, which is not an
--   assumption made by Text.PrettyPrint. But in practice this is often
--   good enough.
class Pretty x
pretty :: Pretty x => x -> Doc

-- | A class used to do proper parenthesization of formulas. If we nest a
--   higher precedence formula inside a lower one parentheses can be
--   omitted. Because <tt>|</tt> has lower precedence than <tt>&amp;</tt>,
--   the formula <tt>a | (b &amp; c)</tt> appears as <tt>a | b &amp;
--   c</tt>, while <tt>(a | b) &amp; c</tt> appears unchanged. (Name
--   Precedence chosen because Fixity was taken.)
--   
--   The second field of Fixity is the FixityDirection, which can be left,
--   right, or non. A left associative operator like <tt>/</tt> is grouped
--   left to right, so parenthese can be omitted from <tt>(a <i> b) </i>
--   c</tt> but not from <tt>a <i> (b </i> c)</tt>. It is a syntax error to
--   omit parentheses when formatting a non-associative operator.
--   
--   The Haskell FixityDirection type is concerned with how to interpret a
--   formula formatted in a certain way, but here we are concerned with how
--   to format a formula given its interpretation. As such, one case the
--   Haskell type does not capture is whether the operator follows the
--   associative law, so we can omit parentheses in an expression such as
--   <tt>a &amp; b &amp; c</tt>.
class HasFixity x
fixity :: HasFixity x => x -> Fixity
data Fixity :: *
Fixity :: Int -> FixityDirection -> Fixity
data FixityDirection :: *
InfixL :: FixityDirection
InfixR :: FixityDirection
InfixN :: FixityDirection

-- | This is used as the initial value for the parent fixity.
topFixity :: Fixity

-- | This is used as the fixity for things that never need
--   parenthesization, such as function application.
botFixity :: Fixity
instance Pretty String


-- | Class Logic defines the basic boolean logic operations, AND, OR, NOT,
--   and so on. Definitions which pertain to both propositional and first
--   order logic are here.
module Data.Logic.Classes.Combine

-- | A type class for logical formulas. Minimal implementation: <tt> (.|.)
--   </tt>
class Negatable formula => Combinable formula where x .&. y = (.~.) ((.~.) x .|. (.~.) y) x .<=>. y = (x .=>. y) .&. (y .=>. x) x .=>. y = ((.~.) x .|. y) x .<=. y = y .=>. x x .<~>. y = ((.~.) x .&. y) .|. (x .&. (.~.) y) x .~|. y = (.~.) (x .|. y) x .~&. y = (.~.) (x .&. y)
(.|.) :: Combinable formula => formula -> formula -> formula
(.&.) :: Combinable formula => formula -> formula -> formula
(.<=>.) :: Combinable formula => formula -> formula -> formula
(.=>.) :: Combinable formula => formula -> formula -> formula
(.<=.) :: Combinable formula => formula -> formula -> formula
(.<~>.) :: Combinable formula => formula -> formula -> formula
(.~|.) :: Combinable formula => formula -> formula -> formula
(.~&.) :: Combinable formula => formula -> formula -> formula

-- | <a>Combination</a> is a helper type used in the signatures of the
--   <tt>foldPropositional</tt> and <tt>foldFirstOrder</tt> methods so can
--   represent all the ways that formulas can be combined using boolean
--   logic - negation, logical And, and so forth.
data Combination formula
BinOp :: formula -> BinOp -> formula -> Combination formula
(:~:) :: formula -> Combination formula

-- | A helper function for building folds: <tt> foldPropositional combine
--   atomic </tt> is a no-op.
combine :: Combinable formula => Combination formula -> formula

-- | Represents the boolean logic binary operations, used in the
--   Combination type above.
data BinOp

-- | Equivalence
(:<=>:) :: BinOp

-- | Implication
(:=>:) :: BinOp

-- | AND
(:&:) :: BinOp

-- | OR
(:|:) :: BinOp
binop :: Combinable formula => formula -> BinOp -> formula -> formula
(∧) :: Combinable formula => formula -> formula -> formula
(∨) :: Combinable formula => formula -> formula -> formula

-- | ⇒ can't be a function when -XUnicodeSyntax is enabled.
(⇒) :: Combinable formula => formula -> formula -> formula
(⇔) :: Combinable formula => formula -> formula -> formula
(==>) :: Combinable formula => formula -> formula -> formula
(<=>) :: Combinable formula => formula -> formula -> formula
prettyBinOp :: BinOp -> Doc
instance Typeable BinOp
instance Typeable Combination
instance Eq BinOp
instance Ord BinOp
instance Data BinOp
instance Enum BinOp
instance Bounded BinOp
instance Show BinOp
instance Read BinOp
instance Eq formula => Eq (Combination formula)
instance Ord formula => Ord (Combination formula)
instance Data formula => Data (Combination formula)
instance Show formula => Show (Combination formula)
instance Read formula => Read (Combination formula)
instance Pretty BinOp

module Data.Logic.Classes.Variable
class (Ord v, IsString v, Data v, Pretty v) => Variable v
variant :: Variable v => v -> Set v -> v
prefix :: Variable v => String -> v -> v
prettyVariable :: Variable v => v -> Doc

-- | Return an infinite list of variations on v
variants :: Variable v => v -> [v]
showVariable :: Variable v => v -> String

module Data.Logic.Classes.Skolem

-- | This class shows how to convert between atomic Skolem functions and
--   Ints. We include a variable type as a parameter because we create
--   skolem functions to replace an existentially quantified variable, and
--   it can be helpful to retain a reference to the variable.
class Variable v => Skolem f v | f -> v
toSkolem :: Skolem f v => v -> f
isSkolem :: Skolem f v => f -> Bool

module Data.Logic.Classes.Term
class (Ord term, Variable v, Function f v) => Term term v f | term -> v f
vt :: Term term v f => v -> term
fApp :: Term term v f => f -> [term] -> term
foldTerm :: Term term v f => (v -> r) -> (f -> [term] -> r) -> term -> r
zipTerms :: Term term v f => (v -> v -> Maybe r) -> (f -> [term] -> f -> [term] -> Maybe r) -> term -> term -> Maybe r
class (Eq f, Ord f, Skolem f v, Data f, Pretty f) => Function f v
convertTerm :: (Term term1 v1 f1, Term term2 v2 f2) => (v1 -> v2) -> (f1 -> f2) -> term1 -> term2
showTerm :: (Term term v f, Show v, Show f) => term -> String
prettyTerm :: Term term v f => (v -> Doc) -> (f -> Doc) -> term -> Doc
fvt :: (Term term v f, Ord v) => term -> Set v
tsubst :: (Term term v f, Ord v) => Map v term -> term -> term
funcs :: (Term term v f, Ord f) => term -> Set (f, Int)

module Data.Logic.Harrison.Unif
unify :: Term term v f => Map v term -> [(term, term)] -> Failing (Map v term)
solve :: Term term v f => Map v term -> Map v term
fullUnify :: Term term v f => [(term, term)] -> Failing (Map v term)
unifyAndApply :: Term term v f => [(term, term)] -> Failing [(term, term)]

module Data.Logic.Types.Common
instance Variable String

module Data.Logic.Classes.Formula
class Formula formula atom | formula -> atom
atomic :: Formula formula atom => atom -> formula
foldAtoms :: (Formula formula atom, Formula formula atom) => (r -> atom -> r) -> r -> formula -> r
mapAtoms :: (Formula formula atom, Formula formula atom) => (atom -> formula) -> formula -> formula

module Data.Logic.Classes.Constants

-- | Some types in the Logic class heirarchy need to have True and False
--   elements.
class Constants p
asBool :: Constants p => p -> Maybe Bool
fromBool :: Constants p => Bool -> p
ifElse :: a -> a -> Bool -> a
true :: Constants p => p
(⊨) :: Constants formula => formula
false :: Constants p => p
(⊭) :: Constants formula => formula
prettyBool :: Bool -> Doc
instance Pretty Bool


-- | PropositionalFormula is a multi-parameter type class for representing
--   instance of propositional (aka zeroth order) logic datatypes. These
--   are formulas which have truth values, but no "for all" or "there
--   exists" quantifiers and thus no variables or terms as we have in first
--   order or predicate logic. It is intended that we will be able to write
--   instances for various different implementations to allow these systems
--   to interoperate. The operator names were adopted from the Logic-TPTP
--   package.
module Data.Logic.Classes.Propositional

-- | A type class for propositional logic. If the type we are writing an
--   instance for is a zero-order (aka propositional) logic type there will
--   generally by a type or a type parameter corresponding to atom. For
--   first order or predicate logic types, it is generally easiest to just
--   use the formula type itself as the atom type, and raise errors in the
--   implementation if a non-atomic formula somehow appears where an atomic
--   formula is expected (i.e. as an argument to atomic or to the third
--   argument of foldPropositional.)
--   
--   The Ord superclass is required so we can put formulas in sets during
--   the normal form computations. Negatable and Combinable are also
--   considered basic operations that we can't build this package without.
--   It is less obvious whether Constants is always required, but the
--   implementation of functions like simplify would be more elaborate if
--   we didn't have it, so we will require it.
class (Ord formula, Negatable formula, Combinable formula, Constants formula, Pretty formula, HasFixity formula, Formula formula atom) => PropositionalFormula formula atom | formula -> atom
foldPropositional :: PropositionalFormula formula atom => (Combination formula -> r) -> (Bool -> r) -> (atom -> r) -> formula -> r

-- | Show a formula in a format that can be evaluated
showPropositional :: PropositionalFormula formula atom => (atom -> String) -> formula -> String

-- | Show a formula in a visually pleasing format.
prettyPropositional :: (PropositionalFormula formula atom, HasFixity formula) => (atom -> Doc) -> Fixity -> formula -> Doc
fixityPropositional :: (HasFixity atom, PropositionalFormula formula atom) => formula -> Fixity

-- | Convert any instance of a propositional logic expression to any other
--   using the supplied atom conversion function.
convertProp :: (PropositionalFormula formula1 atom1, PropositionalFormula formula2 atom2) => (atom1 -> atom2) -> formula1 -> formula2

-- | A helper function for building folds: <tt> foldPropositional combine
--   atomic </tt> is a no-op.
combine :: Combinable formula => Combination formula -> formula

-- | Simplify and recursively apply nnf.
negationNormalForm :: PropositionalFormula formula atom => formula -> formula
clauseNormalForm :: PropositionalFormula formula atom => formula -> formula
clauseNormalForm' :: PropositionalFormula formula atom => formula -> Set (Set formula)
clauseNormalFormAlt :: PropositionalFormula formula atom => formula -> formula

-- | I'm not sure of the clauseNormalForm functions above are wrong or just
--   different.
clauseNormalFormAlt' :: PropositionalFormula formula atom => formula -> Set (Set formula)
disjunctiveNormalForm :: PropositionalFormula formula atom => formula -> formula
disjunctiveNormalForm' :: (PropositionalFormula formula atom, Eq formula) => formula -> Set (Set formula)

-- | Deprecated - use foldAtoms.
overatoms :: PropositionalFormula formula atom => (atom -> r -> r) -> formula -> r -> r

-- | Use this to implement foldAtoms
foldAtomsPropositional :: PropositionalFormula pf atom => (r -> atom -> r) -> r -> pf -> r
mapAtomsPropositional :: PropositionalFormula formula atom => (atom -> formula) -> formula -> formula
instance SafeCopy formula0 => SafeCopy (Combination formula0)
instance SafeCopy BinOp

module Data.Logic.Classes.Literal

-- | Literals are the building blocks of the clause and implicative normal
--   |forms. They support negation and must include True and False
--   elements.
class (Negatable lit, Constants lit, HasFixity atom, Formula lit atom, Ord lit) => Literal lit atom | lit -> atom
foldLiteral :: Literal lit atom => (lit -> r) -> (Bool -> r) -> (atom -> r) -> lit -> r
zipLiterals :: Literal lit atom => (lit -> lit -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (atom -> atom -> Maybe r) -> lit -> lit -> Maybe r
toPropositional :: (Literal lit atom, PropositionalFormula pf atom2) => (atom -> atom2) -> lit -> pf
prettyLit :: Literal lit atom => (Int -> atom -> Doc) -> (v -> Doc) -> Int -> lit -> Doc
foldAtomsLiteral :: Literal lit atom => (r -> atom -> r) -> r -> lit -> r

module Data.Logic.Classes.FirstOrder

-- | The <a>FirstOrderFormula</a> type class. Minimal implementation:
--   <tt>for_all, exists, foldFirstOrder, foldTerm, (.=.), pApp0-pApp7,
--   fApp, var</tt>. 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
--   <tt>No instance for (FirstOrderFormula Formula atom V)</tt> because
--   the function doesn't mention the Term type.
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
for_all :: FirstOrderFormula formula atom v => v -> formula -> formula
exists :: FirstOrderFormula formula atom v => v -> formula -> formula
foldFirstOrder :: FirstOrderFormula formula atom v => (Quant -> v -> formula -> r) -> (Combination formula -> r) -> (Bool -> r) -> (atom -> r) -> formula -> r

-- | The <a>Quant</a> and <tt>InfixPred</tt> types, like the BinOp type in
--   <a>Propositional</a>, could be additional parameters to the type
--   class, but it would add additional complexity with unclear benefits.
data Quant
Forall :: Quant
Exists :: 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

-- | for_all with a list of variables, for backwards compatibility.
for_all' :: FirstOrderFormula formula atom v => [v] -> formula -> formula

-- | exists with a list of variables, for backwards compatibility.
exists' :: FirstOrderFormula formula atom v => [v] -> formula -> formula

-- | Helper function for building folds.
quant :: FirstOrderFormula formula atom v => Quant -> 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
(∃) :: FirstOrderFormula formula atom v => 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'.)
quant' :: FirstOrderFormula formula atom v => Quant -> [v] -> formula -> formula
convertFOF :: (FirstOrderFormula formula1 atom1 v1, FirstOrderFormula formula2 atom2 v2) => (atom1 -> atom2) -> (v1 -> v2) -> 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.
toPropositional :: (FirstOrderFormula formula1 atom v, PropositionalFormula formula2 atom2) => (atom -> atom2) -> formula1 -> formula2

-- | 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.
withUnivQuants :: FirstOrderFormula formula atom v => ([v] -> formula -> r) -> formula -> r

-- | Display a formula in a format that can be read into the interpreter.
showFirstOrder :: (FirstOrderFormula formula atom v, Show v) => (atom -> String) -> formula -> String
prettyFirstOrder :: 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 :: FirstOrderFormula formula atom v => (atom -> formula) -> formula -> formula

-- | Deprecated - use mapAtoms
onatoms :: FirstOrderFormula formula atom v => (atom -> formula) -> formula -> formula

-- | Deprecated - use foldAtoms
overatoms :: FirstOrderFormula formula atom v => (atom -> r -> r) -> formula -> r -> r
atom_union :: (FirstOrderFormula formula atom v, Ord a) => (atom -> Set a) -> formula -> Set a

-- | 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.
fromFirstOrder :: (Formula lit atom2, FirstOrderFormula formula atom v, Literal lit atom2) => (atom -> atom2) -> formula -> Failing lit
fromLiteral :: (Literal lit atom, FirstOrderFormula fof atom2 v) => (atom -> atom2) -> lit -> fof
instance SafeCopy Quant
instance Typeable Quant
instance Eq Quant
instance Ord Quant
instance Show Quant
instance Read Quant
instance Data Quant
instance Enum Quant
instance Bounded Quant

module Data.Logic.Harrison.Formulas.FirstOrder
antecedent :: FirstOrderFormula formula atom v => formula -> formula
consequent :: FirstOrderFormula formula atom v => formula -> formula
on_atoms :: FirstOrderFormula formula atom v => (atom -> formula) -> formula -> formula
over_atoms :: FirstOrderFormula formula atom v => (atom -> b -> b) -> formula -> b -> b
atom_union :: (FirstOrderFormula formula atom v, Ord b) => (atom -> Set b) -> formula -> Set b

module Data.Logic.Harrison.Formulas.Propositional
antecedent :: PropositionalFormula formula atomic => formula -> formula
consequent :: PropositionalFormula formula atomic => formula -> formula
on_atoms :: PropositionalFormula formula atomic => (atomic -> formula) -> formula -> formula
over_atoms :: PropositionalFormula formula atomic => (atomic -> b -> b) -> formula -> b -> b
atom_union :: (PropositionalFormula formula atomic, Ord b) => (atomic -> Set b) -> formula -> Set b

module Data.Logic.Harrison.Prop
eval :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Map atomic Bool -> Bool
atoms :: Ord atomic => PropositionalFormula formula atomic => formula -> Set atomic
onAllValuations :: Ord a => (r -> r -> r) -> (Map a Bool -> r) -> Map a Bool -> Set a -> r
type TruthTable a = ([a], [TruthTableRow])
type TruthTableRow = ([Bool], Bool)
truthTable :: (PropositionalFormula formula atom, Eq atom, Ord atom) => formula -> TruthTable atom
tautology :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Bool
unsatisfiable :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Bool
satisfiable :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Bool
rawdnf :: PropositionalFormula formula atomic => formula -> formula
purednf :: (PropositionalFormula pf atom, Literal lit atom, Ord lit) => pf -> Set (Set lit)
dnf :: (PropositionalFormula pf atom, Literal lit atom, Ord lit) => Set (Set lit) -> pf
dnf' :: (PropositionalFormula pf atom, Literal pf atom) => pf -> pf
trivial :: (Literal lit atom, Ord lit) => Set lit -> Bool
psimplify :: (PropositionalFormula formula atomic, Eq formula) => formula -> formula
nnf :: (PropositionalFormula formula atomic, Eq formula) => formula -> formula
simpdnf :: (PropositionalFormula pf atom, Literal lit atom, Ord lit) => pf -> Set (Set lit)
simpcnf :: (PropositionalFormula pf atom, Literal lit atom, Ord lit) => pf -> Set (Set lit)
positive :: Literal lit atom => lit -> Bool
negative :: Literal lit atom => lit -> Bool
negate :: PropositionalFormula formula atomic => formula -> formula
distrib :: PropositionalFormula formula atomic => formula -> formula
list_disj :: PropositionalFormula formula atomic => Set formula -> formula
list_conj :: (PropositionalFormula formula atomic, Ord formula) => Set formula -> formula
pSubst :: (PropositionalFormula formula atomic, Ord atomic) => Map atomic formula -> formula -> formula
dual :: PropositionalFormula formula atomic => formula -> formula
nenf :: (PropositionalFormula formula atomic, Eq formula) => formula -> formula
mkLits :: (PropositionalFormula formula atomic, Ord formula, Ord atomic) => Set formula -> Map atomic Bool -> formula
allSatValuations :: Ord a => (Map a Bool -> Bool) -> Map a Bool -> Set a -> [Map a Bool]
dnf0 :: (PropositionalFormula formula atomic, Ord atomic, Ord formula) => formula -> formula
cnf :: (PropositionalFormula pf atom, Literal lit atom, Ord lit) => Set (Set lit) -> pf
cnf' :: (PropositionalFormula pf atom, Literal pf atom) => pf -> pf

module Data.Logic.Types.Propositional

-- | The range of a formula is {True, False} when it has no free variables.
data Formula atom
Combine :: (Combination (Formula atom)) -> Formula atom
Atom :: atom -> Formula atom
T :: Formula atom
F :: Formula atom
instance Typeable Formula
instance Eq atom => Eq (Formula atom)
instance Ord atom => Ord (Formula atom)
instance Data atom => Data (Formula atom)
instance (Pretty atom, HasFixity atom, Ord atom) => HasFixity (Formula atom)
instance (Pretty atom, HasFixity atom, Ord atom) => Pretty (Formula atom)
instance (Formula (Formula atom) atom, Pretty atom, HasFixity atom, Ord atom) => PropositionalFormula (Formula atom) atom
instance (Pretty atom, HasFixity atom, Ord atom) => Literal (Formula atom) atom
instance (Pretty atom, HasFixity atom, Ord atom) => Formula (Formula atom) atom
instance Constants (Formula atom)
instance Ord atom => Combinable (Formula atom)
instance Negatable (Formula atom)

module Data.Logic.Harrison.PropExamples
data Atom a
P :: String -> a -> (Maybe a) -> Atom a
type N = Int
prime :: (PropositionalFormula formula (Atom N), Ord formula) => N -> formula
ramsey :: (PropositionalFormula formula (Atom N), Ord formula) => Int -> Int -> N -> formula
tests :: Test
instance Show (Formula (Atom Int))
instance Eq a => Eq (Atom a)
instance Ord a => Ord (Atom a)
instance Show a => Show (Atom a)
instance HasFixity (Atom N)
instance Pretty (Atom N)

module Data.Logic.Harrison.DefCNF
data Atom a
P :: a -> Atom a
class NumAtom atom
ma :: NumAtom atom => N -> atom
ai :: NumAtom atom => atom -> N
mkprop :: (PropositionalFormula pf atom, NumAtom atom) => N -> (pf, N)
maincnf :: (NumAtom atom, PropositionalFormula pf atom) => (pf, Map pf pf, Int) -> (pf, Map pf pf, Int)
defstep :: (PropositionalFormula pf atom, NumAtom atom, Ord pf) => (pf -> pf -> pf) -> (pf, pf) -> (pf, Map pf pf, Int) -> (pf, Map pf pf, Int)
max_varindex :: NumAtom atom => atom -> Int -> Int
mk_defcnf :: (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => ((pf, Map pf pf, Int) -> (pf, Map pf pf, Int)) -> pf -> Set (Set lit)
defcnf1 :: (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => lit -> atom -> pf -> pf
subcnf :: (PropositionalFormula pf atom, NumAtom atom) => ((pf, Map pf pf, Int) -> (pf, Map pf pf, Int)) -> (pf -> pf -> pf) -> pf -> pf -> (pf, Map pf pf, Int) -> (pf, Map pf pf, Int)
orcnf :: (NumAtom atom, PropositionalFormula pf atom) => (pf, Map pf pf, Int) -> (pf, Map pf pf, Int)
andcnf :: (PropositionalFormula pf atom, NumAtom atom, Ord pf) => (pf, Map pf pf, Int) -> (pf, Map pf pf, Int)
defcnfs :: (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => pf -> Set (Set lit)
defcnf2 :: (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => lit -> atom -> pf -> pf
andcnf3 :: (PropositionalFormula pf atom, NumAtom atom, Ord pf) => (pf, Map pf pf, Int) -> (pf, Map pf pf, Int)
defcnf3 :: (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => lit -> atom -> pf -> pf
instance NumAtom (Atom N)

module Data.Logic.Types.Harrison.Formulas.FirstOrder
data Formula a
F :: Formula a
T :: Formula a
Atom :: a -> Formula a
Not :: (Formula a) -> Formula a
And :: (Formula a) -> (Formula a) -> Formula a
Or :: (Formula a) -> (Formula a) -> Formula a
Imp :: (Formula a) -> (Formula a) -> Formula a
Iff :: (Formula a) -> (Formula a) -> Formula a
Forall :: String -> (Formula a) -> Formula a
Exists :: String -> (Formula a) -> Formula a
instance Eq a => Eq (Formula a)
instance Ord a => Ord (Formula a)
instance FirstOrderFormula (Formula a) a String => Pretty (Formula a)
instance (Formula (Formula a) a, Constants a, Pretty a, HasFixity a) => FirstOrderFormula (Formula a) a String
instance (Constants a, Pretty a, HasFixity a) => Formula (Formula a) a
instance Combinable (Formula a)
instance Constants (Formula a)
instance Negatable (Formula atom)

module Data.Logic.Types.Harrison.Formulas.Propositional
data Formula a
F :: Formula a
T :: Formula a
Atom :: a -> Formula a
Not :: (Formula a) -> Formula a
And :: (Formula a) -> (Formula a) -> Formula a
Or :: (Formula a) -> (Formula a) -> Formula a
Imp :: (Formula a) -> (Formula a) -> Formula a
Iff :: (Formula a) -> (Formula a) -> Formula a
instance Eq a => Eq (Formula a)
instance Ord a => Ord (Formula a)
instance (Pretty atom, HasFixity atom, Ord atom) => HasFixity (Formula atom)
instance (Pretty atom, HasFixity atom, Ord atom) => Pretty (Formula atom)
instance (HasFixity atom, Pretty atom, Ord atom) => Literal (Formula atom) atom
instance (Combinable (Formula atom), Pretty atom, HasFixity atom, Ord atom) => PropositionalFormula (Formula atom) atom
instance (Pretty atom, HasFixity atom, Ord atom) => Formula (Formula atom) atom
instance Combinable (Formula a)
instance Constants (Formula a)
instance Negatable (Formula atom)

module Data.Logic.Types.Harrison.Prop
newtype Prop
P :: String -> Prop
pname :: Prop -> String
instance Typeable Prop
instance Read Prop
instance Data Prop
instance Eq Prop
instance Ord Prop
instance Show (Formula String)
instance Show (Formula Prop)
instance HasFixity Prop
instance HasFixity String
instance Pretty Prop
instance Show Prop

module Data.Logic.Classes.Arity

-- | A class that characterizes how many arguments a predicate or function
--   takes. Depending on the context, a result of Nothing may mean that the
--   arity is undetermined or unknown. However, even if this returns
--   Nothing, the same number of arguments must be passed to all uses of a
--   given predicate or function.
class Arity p
arity :: Arity p => p -> Maybe Int


-- | The Apply class represents a type of atom the only supports predicate
--   application.
module Data.Logic.Classes.Apply
class Predicate p => Apply atom p term | atom -> p term
foldApply :: Apply atom p term => (p -> [term] -> r) -> (Bool -> r) -> atom -> r
apply' :: Apply atom p term => p -> [term] -> atom
class (Arity p, Constants p, Eq p, Ord p, Data p, Pretty p) => Predicate p

-- | apply' with an arity check - clients should always call this.
apply :: Apply atom p term => p -> [term] -> atom
zipApplys :: Apply atom p term => (p -> [term] -> p -> [term] -> Maybe r) -> (Bool -> Bool -> Maybe r) -> atom -> atom -> Maybe r
apply0 :: Apply atom p term => p -> atom
apply1 :: Apply atom p term => p -> term -> atom
apply2 :: Apply atom p term => p -> term -> term -> atom
apply3 :: Apply atom p term => p -> term -> term -> term -> atom
apply4 :: Apply atom p term => p -> term -> term -> term -> term -> atom
apply5 :: Apply atom p term => p -> term -> term -> term -> term -> term -> atom
apply6 :: Apply atom p term => p -> term -> term -> term -> term -> term -> term -> atom
apply7 :: Apply atom p term => p -> term -> term -> term -> term -> term -> term -> term -> atom
showApply :: (Apply atom p term, Term term v f, Show v, Show p, Show f) => atom -> String
prettyApply :: (Apply atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> Doc

-- | Return the variables that occur in an instance of Apply.
varApply :: (Apply atom p term, Term term v f) => atom -> Set v
substApply :: (Apply atom p term, Constants atom, Term term v f) => Map v term -> atom -> atom
pApp :: (Formula formula atom, Apply atom p term) => p -> [term] -> formula

-- | Versions of pApp specialized for different argument counts.
pApp0 :: (Formula formula atom, Apply atom p term) => p -> formula
pApp1 :: (Formula formula atom, Apply atom p term) => p -> term -> formula
pApp2 :: (Formula formula atom, Apply atom p term) => p -> term -> term -> formula
pApp3 :: (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> formula
pApp4 :: (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> formula
pApp5 :: (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> formula
pApp6 :: (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> formula
pApp7 :: (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula


-- | Support for equality.
module Data.Logic.Classes.Equals

-- | Its not safe to make Atom a superclass of AtomEq, because the Atom
--   methods will fail on AtomEq instances.
class Predicate p => AtomEq atom p term | atom -> term, atom -> p
foldAtomEq :: AtomEq atom p term => (p -> [term] -> r) -> (Bool -> r) -> (term -> term -> r) -> atom -> r
equals :: AtomEq atom p term => term -> term -> atom
applyEq' :: AtomEq atom p term => p -> [term] -> atom

-- | applyEq' with an arity check - clients should always call this.
applyEq :: AtomEq atom p term => p -> [term] -> atom

-- | A way to represent any predicate's name. Frequently the equality
--   predicate has no standalone representation in the p type, it is just a
--   constructor in the atom type, or even the formula type.
data PredicateName p
Named :: p -> Int -> PredicateName p
Equals :: PredicateName p
zipAtomsEq :: AtomEq atom p term => (p -> [term] -> p -> [term] -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (term -> term -> term -> term -> Maybe r) -> atom -> atom -> Maybe r
apply0 :: AtomEq atom p term => p -> atom
apply1 :: AtomEq atom p a => p -> a -> atom
apply2 :: AtomEq atom p a => p -> a -> a -> atom
apply3 :: AtomEq atom p a => p -> a -> a -> a -> atom
apply4 :: AtomEq atom p a => p -> a -> a -> a -> a -> atom
apply5 :: AtomEq atom p a => p -> a -> a -> a -> a -> a -> atom
apply6 :: AtomEq atom p a => p -> a -> a -> a -> a -> a -> a -> atom
apply7 :: AtomEq atom p a => p -> a -> a -> a -> a -> a -> a -> a -> atom
pApp :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> [term] -> formula

-- | Versions of pApp specialized for different argument counts.
pApp0 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> formula
pApp1 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> formula
pApp2 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> formula
pApp3 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> formula
pApp4 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> formula
pApp5 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> formula
pApp6 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> formula
pApp7 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula
showFirstOrderFormulaEq :: (FirstOrderFormula fof atom v, AtomEq atom p term, Show term, Show v, Show p) => fof -> String
(.=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
(≡) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
(.!=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
(≢) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
fromAtomEq :: (AtomEq atom1 p1 term1, Term term1 v1 f1, AtomEq atom2 p2 term2, Term term2 v2 f2, Constants atom2) => (v1 -> v2) -> (p1 -> p2) -> (f1 -> f2) -> atom1 -> atom2
showAtomEq :: (AtomEq atom p term, Term term v f, Show v, Show p, Show f) => atom -> String
prettyAtomEq :: (AtomEq atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> Doc

-- | Return the variables that occur in an instance of AtomEq.
varAtomEq :: (AtomEq atom p term, Term term v f) => atom -> Set v
substAtomEq :: (AtomEq atom p term, Constants atom, Term term v f) => Map v term -> atom -> atom
funcsAtomEq :: (AtomEq atom p term, Term term v f, Ord f) => atom -> Set (f, Int)
instance Eq p => Eq (PredicateName p)
instance Ord p => Ord (PredicateName p)
instance Show p => Show (PredicateName p)
instance (Pretty p, Ord p) => Pretty (PredicateName p)

module Data.Logic.Harrison.Equal
predicates :: (FirstOrderFormula formula atom v, AtomEq atom p term, Ord p) => formula -> Set (PredicateName p)
function_congruence :: (FirstOrderFormula fof atom v, AtomEq atom p term, Term term v f) => (f, Int) -> Set fof
predicate_congruence :: (FirstOrderFormula fof atom v, AtomEq atom p term, Term term v f, Ord p) => PredicateName p -> Set fof
equivalence_axioms :: (FirstOrderFormula fof atom v, AtomEq atom p term, Term term v f, Ord fof) => Set fof
equalitize :: (FirstOrderFormula formula atom v, Formula formula atom, AtomEq atom p term, Ord p, Show p, Term term v f, Ord formula, Ord f) => formula -> formula
functions' :: (Formula formula atom, Ord f) => (atom -> Set (f, Int)) -> formula -> Set (f, Int)

module Data.Logic.Harrison.FOL
eval :: FirstOrderFormula formula atom v => formula -> (atom -> Bool) -> Bool
list_disj :: (Constants formula, Combinable formula) => Set formula -> formula
list_conj :: (Constants formula, Combinable formula) => Set formula -> formula

-- | Return all variables occurring in a formula.
var :: (FirstOrderFormula formula atom v, Atom atom term v) => formula -> Set v

-- | Return the variables that occur free in a formula.
fv :: (FirstOrderFormula formula atom v, Atom atom term v) => formula -> Set v
subst :: (FirstOrderFormula formula atom v, Term term v f, Atom atom term v) => Map v term -> formula -> formula
generalize :: (FirstOrderFormula formula atom v, Atom atom term v) => formula -> formula

module Data.Logic.Harrison.Skolem
simplify :: (FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> fof

-- | Just looks for double negatives and negated constants.
lsimplify :: Literal lit atom => lit -> lit
nnf :: FirstOrderFormula formula atom v => formula -> formula

-- | Convert to Prenex normal form, with all quantifiers at the left.
pnf :: (FirstOrderFormula formula atom v, Atom atom term v, Term term v f) => formula -> formula
functions :: (Formula formula atom, Ord f) => (atom -> Set (f, Int)) -> formula -> Set (f, Int)

-- | The Skolem monad transformer
type SkolemT v term m = StateT (SkolemState v term) m

-- | The Skolem monad
type Skolem v term = StateT (SkolemState v term) Identity

-- | Run a computation in the Skolem monad.
runSkolem :: SkolemT v term Identity a -> a

-- | Run a computation in a stacked invocation of the Skolem monad.
runSkolemT :: Monad m => SkolemT v term m a -> m a

-- | Remove the leading universal quantifiers. After a call to pnf this
--   will be all the universal quantifiers, and the skolemization will have
--   already turned all the existential quantifiers into skolem functions.
specialize :: FirstOrderFormula fof atom v => fof -> fof

-- | Skolemize and then specialize. Because we know all quantifiers are
--   gone we can convert to any instance of PropositionalFormula.
skolemize :: (Monad m, FirstOrderFormula fof atom v, PropositionalFormula pf atom2, Atom atom term v, Term term v f, Eq pf) => (atom -> atom2) -> fof -> SkolemT v term m pf

-- | I need to consult the Harrison book for the reasons why we don't |just
--   Skolemize the result of prenexNormalForm.
askolemize :: (Monad m, FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> SkolemT v term m fof

-- | We get Skolem Normal Form by skolemizing and then converting to Prenex
--   Normal Form, and finally eliminating the remaining quantifiers.
skolemNormalForm :: (FirstOrderFormula fof atom v, PropositionalFormula pf atom2, Atom atom term v, Term term v f, Monad m, Ord fof, Eq pf) => (atom -> atom2) -> fof -> SkolemT v term m pf

-- | Skolemize the formula by removing the existential quantifiers and
--   replacing the variables they quantify with skolem functions (and
--   constants, which are functions of zero variables.) The Skolem
--   functions are new functions (obtained from the SkolemT monad) which
--   are applied to the list of variables which are universally quantified
--   in the context where the existential quantifier appeared.
skolem :: (Monad m, FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> SkolemT v term m fof


-- | Versions of the normal form functions in Prop for FirstOrderFormula.
module Data.Logic.Harrison.Normal
trivial :: (Negatable lit, Ord lit) => Set lit -> Bool
simpdnf :: (FirstOrderFormula fof atom v, Eq fof, Ord fof) => fof -> Set (Set fof)
simpdnf' :: (FirstOrderFormula fof atom v, Literal lit atom, Formula lit atom, Ord lit) => fof -> Set (Set lit)
simpcnf :: (FirstOrderFormula fof atom v, Ord fof) => fof -> Set (Set fof)
simpcnf' :: (FirstOrderFormula fof atom v, Literal lit atom, Ord lit) => fof -> Set (Set lit)


-- | A series of transformations to convert first order logic formulas into
--   (ultimately) Clause Normal Form.
--   
--   <pre>
--   1st order formula:
--     ∀Y (∀X (taller(Y,X) | wise(X)) =&gt; wise(Y))
--   
--   Simplify
--     ∀Y (~∀X (taller(Y,X) | wise(X)) | wise(Y))
--   
--   Move negations in - Negation Normal Form
--     ∀Y (∃X (~taller(Y,X) &amp; ~wise(X)) | wise(Y))
--   
--   Move quantifiers out - Prenex Normal Form
--     ∀Y (∃X ((~taller(Y,X) &amp; ~wise(X)) | wise(Y)))
--   
--   Distribute disjunctions
--     ∀Y ∃X ((~taller(Y,X) | wise(Y)) &amp; (~wise(X) | wise(Y)))
--   
--   Skolemize  - Skolem Normal Form
--     ∀Y (~taller(Y,x(Y)) | wise(Y)) &amp; (~wise(x(Y)) | wise(Y))
--   
--   Convert to CNF
--     { ~taller(Y,x(Y)) | wise(Y),
--       ~wise(x(Y)) | wise(Y) } 
--   </pre>
module Data.Logic.Normal.Clause

-- | Convert to Skolem Normal Form and then distribute the disjunctions
--   over the conjunctions:
--   
--   <pre>
--   Formula      Rewrites to
--   P | (Q &amp; R)  (P | Q) &amp; (P | R)
--   (Q &amp; R) | P  (Q | P) &amp; (R | P)
--   </pre>
clauseNormalForm :: (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, Term term v f, Literal lit atom, Ord formula, Ord lit) => formula -> SkolemT v term m (Set (Set lit))
cnfTrace :: (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, AtomEq atom p term, Term term v f, Literal lit atom, Ord formula, Ord lit) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> formula -> SkolemT v term m (String, Set (Set lit))

module Data.Logic.Instances.PropLogic
flatten :: PropForm a -> PropForm a
plSat0 :: (PropAlg a (PropForm formula), PropositionalFormula formula atom, Ord formula) => PropForm formula -> Bool
plSat :: (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, Term term v f, Eq formula, Literal formula atom, Ord formula) => formula -> SkolemT v term m Bool
instance (PropositionalFormula (PropForm atom) atom, HasFixity atom) => HasFixity (PropForm atom)
instance (PropositionalFormula (PropForm atom) atom, Pretty atom, HasFixity atom) => Pretty (PropForm atom)
instance Constants (PropForm formula)
instance (Combinable (PropForm a), Pretty a, HasFixity a, Ord a) => PropositionalFormula (PropForm a) a
instance (Pretty a, HasFixity a, Ord a) => Formula (PropForm a) a
instance Combinable (PropForm a)
instance Negatable (PropForm a)

module Data.Logic.Normal.Implicative
type LiteralMapT f = StateT (Int, Map f Int)

-- | Combination of Normal monad and LiteralMap monad
type NormalT formula v term m a = SkolemT v term (LiteralMapT formula m) a
runNormal :: NormalT formula v term Identity a -> a
runNormalT :: Monad m => NormalT formula v term m a -> m a

-- | A type to represent a formula in Implicative Normal Form. Such a
--   formula has the form <tt>a &amp; b &amp; c .=&gt;. d | e | f</tt>,
--   where a thru f are literals. One more restriction that is not implied
--   by the type is that no literal can appear in both the pos set and the
--   neg set.
data ImplicativeForm lit
INF :: Set lit -> Set lit -> ImplicativeForm lit
neg :: ImplicativeForm lit -> Set lit
pos :: ImplicativeForm lit -> Set lit

-- | A version of MakeINF that takes lists instead of sets, used for
--   implementing a more attractive show method.
makeINF' :: (Negatable lit, Ord lit) => [lit] -> [lit] -> ImplicativeForm lit

-- | Take the clause normal form, and turn it into implicative form, where
--   each clauses becomes an (LHS, RHS) pair with the negated literals on
--   the LHS and the non-negated literals on the RHS: <tt> (a | ~b | c |
--   ~d) becomes (b &amp; d) =&gt; (a | c) (~b | ~d) | (a | c) ~~(~b | ~d)
--   | (a | c) ~(b &amp; d) | (a | c) </tt> If there are skolem functions
--   on the RHS, split the formula using this identity: <tt> (a | b | c)
--   =&gt; (d &amp; e &amp; f) </tt> becomes <tt> a | b | c =&gt; d a | b |
--   c =&gt; e a | b | c =&gt; f </tt>
implicativeNormalForm :: (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, Literal lit atom, Term term v f, Data formula, Ord formula, Ord lit, Data lit, Skolem f v) => formula -> SkolemT v term m (Set (ImplicativeForm lit))
prettyINF :: (Negatable lit, Ord lit) => (lit -> Doc) -> ImplicativeForm lit -> Doc
prettyProof :: (Negatable lit, Ord lit) => (lit -> Doc) -> Set (ImplicativeForm lit) -> Doc
instance Typeable ImplicativeForm
instance Eq lit => Eq (ImplicativeForm lit)
instance Ord lit => Ord (ImplicativeForm lit)
instance (Data lit, Ord lit) => Data (ImplicativeForm lit)
instance Show lit => Show (ImplicativeForm lit)

module Data.Logic.Instances.SatSolver
toCNF :: (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, AtomEq atom p term, Term term v f, Literal formula atom, Ord formula) => formula -> NormalT formula v term m CNF

-- | Convert a [[formula]] to CNF, which means building a map from formula
--   to Literal.
toLiteral :: (Monad m, Negatable lit, Ord lit) => lit -> LiteralMapT lit m Literal
instance Typeable Literal
instance Data Literal
instance ClauseNormalFormula CNF Literal
instance Negatable Literal
instance Ord Literal


-- | Do satisfiability computations on any FirstOrderFormula formula by
--   converting it to a convenient instance of PropositionalFormula and
--   using the satisfiable function from that instance. Currently we use
--   the satisfiable function from the PropLogic package, by the Bucephalus
--   project.
module Data.Logic.Satisfiable

-- | Is there any variable assignment that makes the formula true?
--   satisfiable :: forall formula atom term v f m. (Monad m,
--   FirstOrderFormula formula atom v, Formula atom term v, Term term v f,
--   Ord formula, Literal formula atom v, Ord atom) =&gt; formula -&gt;
--   SkolemT v term m Bool
satisfiable :: (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m Bool

-- | Is the negation of the formula inconsistant?
theorem :: (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m Bool

-- | Is the formula always false? (Not satisfiable.)
inconsistant :: (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m Bool

-- | A formula is invalid if it is neither a theorem nor inconsistent.
invalid :: (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m Bool

module Data.Logic.Harrison.Prolog
renamerule :: (FirstOrderFormula fof atom v, Atom atom term v, Term term v f, Ord fof) => Int -> (Set fof, fof) -> ((Set fof, fof), Int)

module Data.Logic.Types.Harrison.FOL
data TermType
Var :: String -> TermType
Fn :: Function -> [TermType] -> TermType
data FOL
R :: String -> [TermType] -> FOL

-- | The Harrison book uses String for atomic function, but we need
--   something a little more type safe because of our Skolem class.
data Function
FName :: String -> Function
Skolem :: String -> Function
instance Typeable Function
instance Eq Function
instance Ord Function
instance Data Function
instance Show Function
instance Eq TermType
instance Ord TermType
instance Eq FOL
instance Ord FOL
instance Show FOL
instance HasFixity FOL
instance Term TermType String Function
instance Skolem Function String
instance Function Function String
instance Pretty Function
instance Arity String
instance Pretty FOL
instance Predicate String
instance Constants FOL
instance Constants String
instance Apply FOL String TermType
instance Pretty TermType
instance Show TermType

module Data.Logic.HUnit

-- | HUnit Test type with an added phantom type parameter. To run such a
--   test you use the convert function below: <tt> :load
--   Data.Logic.Tests.Harrison.Meson :m +Data.Logic.Tests.HUnit :m
--   +Test.HUnit runTestTT (convert tests) </tt>
data Test t
TestCase :: (Assertion t) -> Test t
TestList :: [Test t] -> Test t
TestLabel :: String -> (Test t) -> Test t
Test0 :: Test -> Test t
type Assertion t = IO ()

-- | Asserts that the specified actual value is equal to the expected
--   value. The output message will contain the prefix, the expected value,
--   and the actual value.
--   
--   If the prefix is the empty string (i.e., <tt>""</tt>), then the prefix
--   is omitted and only the expected and actual values are output.
assertEqual :: (Eq a, Show a) => String -> a -> a -> Assertion
convert :: Test t -> Test
class (FirstOrderFormula formula atom v, Apply atom p term, Term term v f, Eq formula, Ord formula, Show formula, Eq p, IsString v, IsString p, IsString f, Ord f, Ord p, Eq term, Show term, Ord term, Show v) => TestFormula formula atom term v p f
class (FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f, Eq formula, Ord formula, Show formula, Eq p, IsString v, IsString p, IsString f, Ord f, Ord p, Eq term, Show term, Ord term, Show v) => TestFormulaEq formula atom term v p f
instance IsString Function

module Data.Logic.Harrison.DP
tests :: Test
dpll :: (Literal lit atom, Ord lit) => Set (Set lit) -> Failing Bool
instance Eq TrailMix
instance Ord TrailMix
instance NumAtom (Atom N)

module Data.Logic.Harrison.Herbrand
pholds :: (PropositionalFormula formula atom, Ord atom) => (Map atom Bool) -> formula -> Bool
herbfuns :: (PropositionalFormula pf atom, Formula pf atom, Atom atom term v, Term term v f, IsString f, Ord f) => (atom -> Set (f, Int)) -> pf -> (Set (f, Int), Set (f, Int))
groundterms :: Term term v f => Set term -> Set (f, Int) -> Int -> Set term
groundtuples :: Term term v f => Set term -> Set (f, Int) -> Int -> Int -> Set [term]
herbloop :: (Literal lit atom, Term term v f, Atom atom term v) => (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)) -> (Set (Set lit) -> Failing Bool) -> Set (Set lit) -> Set term -> Set (f, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Failing (Set [term])
subst' :: (Literal lit atom, Atom atom term v, Term term v f) => Map v term -> lit -> lit
gilmore_loop :: (Literal lit atom, Term term v f, Atom atom term v, Ord lit) => Set (Set lit) -> Set term -> Set (f, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Failing (Set [term])
gilmore :: (FirstOrderFormula fof atom v, PropositionalFormula pf atom, Literal pf atom, Term term v f, Atom atom term v, IsString f, Ord pf) => pf -> (atom -> Set (f, Int)) -> fof -> Failing Int
dp_mfn :: (Ord b, Ord a) => Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)
dp_loop :: (Literal lit atom, Term term v f, Atom atom term v, Ord lit) => Set (Set lit) -> Set term -> Set (f, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Failing (Set [term])
davisputnam :: (FirstOrderFormula fof atom v, PropositionalFormula lit atom, Literal lit atom, Term term v f, Atom atom term v, IsString f, Ord lit) => lit -> (atom -> Set (f, Int)) -> fof -> Failing Int
dp_refine :: (Literal lit atom, Atom atom term v, Term term v f) => Set (Set lit) -> [v] -> Set [term] -> Set [term] -> Failing (Set [term])
dp_refine_loop :: (Literal lit atom, Term term v f, Atom atom term v) => Set (Set lit) -> Set term -> Set (f, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Failing (Set [term])
davisputnam' :: (FirstOrderFormula fof atom v, Literal lit atom, PropositionalFormula pf atom, Term term v f, Atom atom term v, IsString f) => lit -> pf -> (atom -> Set (f, Int)) -> fof -> Failing Int

module Data.Logic.Harrison.Tableaux
unify_literals :: (Literal lit atom, Atom atom term v, Term term v f) => Map v term -> lit -> lit -> Failing (Map v term)
unifyAtomsEq :: (AtomEq atom p term, Term term v f) => Map v term -> atom -> atom -> Failing (Map v term)

-- | Try f with higher and higher values of n until it succeeds, or
--   optional maximum depth limit is exceeded.
deepen :: (Int -> Failing t) -> Int -> Maybe Int -> Failing (t, Int)

module Data.Logic.Harrison.Meson
contrapositives :: (FirstOrderFormula fof atom v, Ord fof) => Set fof -> Set (Set fof, fof)
mexpand :: (FirstOrderFormula fof atom v, Literal fof atom, Term term v f, Atom atom term v, Ord fof) => Set (Set fof, fof) -> Set fof -> fof -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int)) -> (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
puremeson :: (FirstOrderFormula fof atom v, Literal fof atom, Term term v f, Atom atom term v, Ord fof) => Maybe Int -> fof -> Failing ((Map v term, Int, Int), Int)
meson :: (FirstOrderFormula fof atom v, PropositionalFormula fof atom, Literal fof atom, Term term v f, Atom atom term v, Ord fof, Monad m) => Maybe Int -> fof -> SkolemT v term m (Set (Failing ((Map v term, Int, Int), Int)))

module Data.Logic.Harrison.Resolution
resolution1 :: (Literal fof atom, FirstOrderFormula fof atom v, PropositionalFormula fof atom, Term term v f, Atom atom term v, Ord fof, Monad m) => fof -> SkolemT v term m (Set (Failing Bool))
resolution2 :: (Literal fof atom, FirstOrderFormula fof atom v, PropositionalFormula fof atom, Term term v f, Atom atom term v, Ord fof, Monad m) => fof -> SkolemT v term m (Set (Failing Bool))
resolution3 :: (Literal fof atom, FirstOrderFormula fof atom v, PropositionalFormula fof atom, Term term v f, Atom atom term v, Ord fof, Monad m) => fof -> SkolemT v term m (Set (Failing Bool))
presolution :: (Literal fof atom, FirstOrderFormula fof atom v, PropositionalFormula fof atom, Term term v f, Atom atom term v, Ord fof, Monad m) => fof -> SkolemT v term m (Set (Failing Bool))
matchAtomsEq :: (AtomEq atom p term, Term term v f) => Map v term -> atom -> atom -> Failing (Map v term)

module Data.Logic.Instances.Chiou
data Sentence v p f
Connective :: (Sentence v p f) -> Connective -> (Sentence v p f) -> Sentence v p f
Quantifier :: Quantifier -> [v] -> (Sentence v p f) -> Sentence v p f
Not :: (Sentence v p f) -> Sentence v p f
Predicate :: p -> [CTerm v f] -> Sentence v p f
Equal :: (CTerm v f) -> (CTerm v f) -> Sentence v p f
data CTerm v f
Function :: f -> [CTerm v f] -> CTerm v f
Variable :: v -> CTerm v f
data Connective
Imply :: Connective
Equiv :: Connective
And :: Connective
Or :: Connective
data Quantifier
ForAll :: Quantifier
ExistsCh :: Quantifier
data ConjunctiveNormalForm v p f
CNF :: [Sentence v p f] -> ConjunctiveNormalForm v p f
data NormalSentence v p f
NFNot :: (NormalSentence v p f) -> NormalSentence v p f
NFPredicate :: p -> [NormalTerm v f] -> NormalSentence v p f
NFEqual :: (NormalTerm v f) -> (NormalTerm v f) -> NormalSentence v p f
data NormalTerm v f
NormalFunction :: f -> [NormalTerm v f] -> NormalTerm v f
NormalVariable :: v -> NormalTerm v f
toSentence :: (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Atom (Sentence v p f) (CTerm v f) v, Function f v, Variable v, Predicate p) => NormalSentence v p f -> Sentence v p f
fromSentence :: (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Predicate p) => Sentence v p f -> NormalSentence v p f
instance Typeable CTerm
instance Typeable Connective
instance Typeable Quantifier
instance Typeable Sentence
instance Typeable NormalTerm
instance Typeable NormalSentence
instance (Eq v, Eq f) => Eq (CTerm v f)
instance (Ord v, Ord f) => Ord (CTerm v f)
instance (Data v, Data f) => Data (CTerm v f)
instance Eq Connective
instance Ord Connective
instance Show Connective
instance Data Connective
instance Eq Quantifier
instance Ord Quantifier
instance Show Quantifier
instance Data Quantifier
instance (Eq v, Eq p, Eq f) => Eq (Sentence v p f)
instance (Ord v, Ord p, Ord f) => Ord (Sentence v p f)
instance (Data v, Data p, Data f) => Data (Sentence v p f)
instance Eq v => Eq (AtomicFunction v)
instance Show v => Show (AtomicFunction v)
instance (Eq v, Eq p, Eq f) => Eq (ConjunctiveNormalForm v p f)
instance (Eq v, Eq f) => Eq (NormalTerm v f)
instance (Ord v, Ord f) => Ord (NormalTerm v f)
instance (Data v, Data f) => Data (NormalTerm v f)
instance (Eq v, Eq p, Eq f) => Eq (NormalSentence v p f)
instance (Ord v, Ord p, Ord f) => Ord (NormalSentence v p f)
instance (Data v, Data p, Data f) => Data (NormalSentence v p f)
instance (Variable v, Function f v) => Term (NormalTerm v f) v f
instance (Formula (NormalSentence v p f) (NormalSentence v p f), Combinable (NormalSentence v p f), Predicate p, Function f v, Variable v) => HasFixity (NormalSentence v p f)
instance (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
instance (Predicate p, Function f v, Combinable (NormalSentence v p f)) => Formula (NormalSentence v p f) (NormalSentence v p f)
instance (Formula (NormalSentence v p f) (NormalSentence v p f), Variable v, Predicate p, Function f v, Combinable (NormalSentence v p f)) => Pretty (NormalSentence v p f)
instance Negatable (NormalSentence v p f)
instance (Constants p, Eq (NormalSentence v p f)) => Constants (NormalSentence v p f)
instance (Variable v, Function f v) => Term (CTerm v f) v f
instance (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
instance (Formula (Sentence v p f) (Sentence v p f), Predicate p, Function f v, Variable v) => HasFixity (Sentence v p f)
instance (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Variable v, Predicate p, Function f v) => Pretty (Sentence v p f)
instance Predicate p => AtomEq (Sentence v p f) p (CTerm v f)
instance (Variable v, Predicate p, Function f v) => Apply (Sentence v p f) p (CTerm v f)
instance Variable v => Skolem (AtomicFunction v) v
instance IsString (AtomicFunction v)
instance (Formula (Sentence v p f) (Sentence v p f), Variable v, Predicate p, Function f v, Combinable (Sentence v p f)) => PropositionalFormula (Sentence v p f) (Sentence v p f)
instance (Predicate p, Function f v) => Formula (Sentence v p f) (Sentence v p f)
instance (Ord v, Ord p, Ord f) => Combinable (Sentence v p f)
instance (Constants p, Eq (Sentence v p f)) => Constants (Sentence v p f)
instance Negatable (Sentence v p f)

module Data.Logic.Resolution
prove :: (Literal lit atom, Atom atom term v, Term term v f, Ord lit, Ord term, Ord v, AtomEq atom p term, Predicate p) => Maybe Int -> SetOfSupport lit v term -> SetOfSupport lit v term -> Set (ImplicativeForm lit) -> (Bool, SetOfSupport lit v term)

-- | Convert the "question" to a set of support.
getSetOfSupport :: (Literal lit atom, Atom atom term v, Term term v f, Ord lit, Ord term, Ord v) => Set (ImplicativeForm lit) -> Set (ImplicativeForm lit, Map v term)
type SetOfSupport lit v term = Set (Unification lit v term)
type Unification lit v term = (ImplicativeForm lit, Map v term)
isRenameOfAtomEq :: (AtomEq atom p term, Term term v f) => atom -> atom -> Bool
getSubstAtomEq :: (AtomEq atom p term, Term term v f) => Map v term -> atom -> Map v term

module Data.Logic.KnowledgeBase
data WithId a
WithId :: a -> Int -> WithId a
wiItem :: WithId a -> a
wiIdent :: WithId a -> Int

-- | A monad for running the knowledge base.
type ProverT inf = StateT (ProverState inf)
runProver' :: Maybe Int -> ProverT' v term inf Identity a -> a
runProverT' :: Monad m => Maybe Int -> ProverT' v term inf m a -> m a

-- | Return the contents of the knowledgebase.
getKB :: Monad m => ProverT inf m (Set (WithId inf))

-- | Remove a particular sentence from the knowledge base
unloadKB :: (Monad m, Ord inf) => SentenceCount -> ProverT inf m (Maybe (KnowledgeBase inf))

-- | Try to prove a sentence, return the result and the proof. askKB should
--   be in KnowledgeBase module. However, since resolution is here
--   functions are here, it is also placed in this module.
askKB :: (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal lit atom, Atom atom term v, AtomEq atom p term, Term term v f, Ord formula, Ord term, Ord lit, Data formula, Data lit) => formula -> ProverT' v term (ImplicativeForm lit) m Bool

-- | Return a flag indicating whether sentence was proved, along with a
--   proof.
theoremKB :: (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal lit atom, Atom atom term v, AtomEq atom p term, Term term v f, Ord formula, Ord term, Ord lit, Data formula, Data lit) => formula -> ProverT' v term (ImplicativeForm lit) m (Bool, SetOfSupport lit v term)

-- | Return a flag indicating whether sentence was disproved, along with a
--   disproof.
inconsistantKB :: (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal lit atom, Atom atom term v, AtomEq atom p term, Term term v f, Monad m, Ord formula, Data formula, Data lit, Eq lit, Ord lit, Ord term) => formula -> ProverT' v term (ImplicativeForm lit) m (Bool, SetOfSupport lit v term)
data ProofResult

-- | The conjecture is unsatisfiable
Disproved :: ProofResult

-- | The negated conjecture is unsatisfiable
Proved :: ProofResult

-- | Both are satisfiable
Invalid :: ProofResult
data Proof lit
Proof :: ProofResult -> Set (ImplicativeForm lit) -> Proof lit
proofResult :: Proof lit -> ProofResult
proof :: Proof lit -> Set (ImplicativeForm lit)

-- | See whether the sentence is true, false or invalid. Return proofs for
--   truth and falsity.
validKB :: (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal lit atom, Atom atom term v, AtomEq atom p term, Term term v f, Monad m, Ord formula, Ord term, Ord lit, Data formula, Data lit) => formula -> ProverT' v term (ImplicativeForm lit) m (ProofResult, SetOfSupport lit v term, SetOfSupport lit v term)

-- | Validate a sentence and insert it into the knowledgebase. Returns the
--   INF sentences derived from the new sentence, or Nothing if the new
--   sentence is inconsistant with the current knowledgebase.
tellKB :: (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal lit atom, Atom atom term v, AtomEq atom p term, Term term v f, Monad m, Ord formula, Data formula, Data lit, Eq lit, Ord lit, Ord term) => formula -> ProverT' v term (ImplicativeForm lit) m (Proof lit)
loadKB :: (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal lit atom, Atom atom term v, AtomEq atom p term, Term term v f, Monad m, Ord formula, Ord term, Ord lit, Data formula, Data lit) => [formula] -> ProverT' v term (ImplicativeForm lit) m [Proof lit]

-- | Delete an entry from the KB.
--   
--   Return a text description of the contents of the knowledgebase.
showKB :: (Show inf, Monad m) => ProverT inf m String
instance Typeable Proof
instance (Data lit, Ord lit) => Data (Proof lit)
instance Eq lit => Eq (Proof lit)
instance Ord lit => Ord (Proof lit)
instance (Ord lit, Show lit, Literal lit atom, FirstOrderFormula lit atom v) => Show (Proof lit)
instance SafeCopy ProofResult
instance Typeable WithId
instance Typeable ProofResult
instance Eq a => Eq (WithId a)
instance Ord a => Ord (WithId a)
instance Show a => Show (WithId a)
instance Data a => Data (WithId a)
instance Data ProofResult
instance Eq ProofResult
instance Ord ProofResult
instance Show ProofResult


-- | Data types which are instances of the Logic type class for use when
--   you just want to use the classes and you don't have a particular
--   representation you need to use.
module Data.Logic.Types.FirstOrder

-- | The range of a formula is {True, False} when it has no free variables.
data Formula v p f
Predicate :: (Predicate p (PTerm v f)) -> Formula v p f
Combine :: (Combination (Formula v p f)) -> Formula v p f
Quant :: Quant -> v -> (Formula v p f) -> Formula v p f

-- | The range of a term is an element of a set.
data PTerm v f

-- | A variable, either free or bound by an enclosing quantifier.
Var :: v -> PTerm v f

-- | Function application. Constants are encoded as nullary functions. The
--   result is another term.
FunApp :: f -> [PTerm v f] -> PTerm v f

-- | A temporary type used in the fold method to represent the combination
--   of a predicate and its arguments. This reduces the number of arguments
--   to foldFirstOrder and makes it easier to manage the mapping of the
--   different instances to the class methods.
data Predicate p term
Equal :: term -> term -> Predicate p term
Apply :: p -> [term] -> Predicate p term
instance (SafeCopy p, SafeCopy term) => Migrate (Predicate p term)
instance (SafeCopy p0, SafeCopy term0) => SafeCopy (Predicate_v1 p0 term0)
instance Typeable Predicate_v1
instance (Eq p, Eq term) => Eq (Predicate_v1 p term)
instance (Ord p, Ord term) => Ord (Predicate_v1 p term)
instance (Data p, Data term) => Data (Predicate_v1 p term)
instance (Show p, Show term) => Show (Predicate_v1 p term)
instance (Read p, Read term) => Read (Predicate_v1 p term)
instance (SafeCopy p0, SafeCopy term0) => SafeCopy (Predicate p0 term0)
instance (SafeCopy v0, SafeCopy p0, SafeCopy f0) => SafeCopy (Formula v0 p0 f0)
instance (SafeCopy v0, SafeCopy f0) => SafeCopy (PTerm v0 f0)
instance Typeable Predicate
instance Typeable PTerm
instance Typeable Formula
instance (Eq p, Eq term) => Eq (Predicate p term)
instance (Ord p, Ord term) => Ord (Predicate p term)
instance (Data p, Data term) => Data (Predicate p term)
instance (Show p, Show term) => Show (Predicate p term)
instance (Read p, Read term) => Read (Predicate p term)
instance (Eq v, Eq f) => Eq (PTerm v f)
instance (Ord v, Ord f) => Ord (PTerm v f)
instance (Data v, Data f) => Data (PTerm v f)
instance (Show v, Show f) => Show (PTerm v f)
instance (Read v, Read f) => Read (PTerm v f)
instance (Eq v, Eq p, Eq f) => Eq (Formula v p f)
instance (Ord v, Ord p, Ord f) => Ord (Formula v p f)
instance (Data v, Data p, Data f) => Data (Formula v p f)
instance (Show v, Show p, Show f) => Show (Formula v p f)
instance (Read v, Read p, Read f) => Read (Formula v p f)
instance HasFixity (Predicate p term)
instance (Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => Pretty (Formula v p f)
instance (Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Variable v, Function f v, HasFixity (Predicate p (PTerm v f))) => HasFixity (Formula v p f)
instance (Variable v, Pretty v, Predicate p, Pretty p, Function f v, Pretty f) => Pretty (Predicate p (PTerm v f))
instance (Predicate p, Variable v, Function f v) => Atom (Predicate p (PTerm v f)) (PTerm v f) v
instance (Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f))) => Literal (Formula v p f) (Predicate p (PTerm v f))
instance (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
instance Predicate p => AtomEq (Predicate p (PTerm v f)) p (PTerm v f)
instance (Variable v, Function f v) => Term (PTerm v f) v f
instance (Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v, Constants (Formula v p f), Combinable (Formula v p f)) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f))
instance (Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f))
instance Constants (Formula v p f) => Combinable (Formula v p f)
instance Constants p => Constants (Predicate p (PTerm v f))
instance Constants p => Constants (Formula v p f)
instance Negatable (Formula v p f)


-- | An instance of FirstOrderFormula which implements Eq and Ord by
--   comparing after conversion to normal form. This helps us notice that
--   formula which only differ in ways that preserve identity, e.g. swapped
--   arguments to a commutative operator.
module Data.Logic.Types.FirstOrderPublic

-- | The new Formula type is just a wrapper around the Native instance
--   (which eventually should be renamed the Internal instance.) No derived
--   Eq or Ord instances.
data Formula v p f
Formula :: Formula v p f -> Formula v p f
unFormula :: Formula v p f -> Formula v p f

-- | Convert between the public and internal representations.
class Bijection p i
public :: Bijection p i => i -> p
intern :: Bijection p i => p -> i
instance (SafeCopy v0, SafeCopy p0, SafeCopy f0) => SafeCopy (Formula v0 p0 f0)
instance Typeable Formula
instance (Data v, Data p, Data f) => Data (Formula v p f)
instance (Show v, Show p, Show f) => Show (Formula v p f)
instance (Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Pretty v, Show v, Variable v, Pretty p, Show p, Predicate p, Pretty f, Show f, Function f v) => Pretty (Formula v p f)
instance (Predicate p, Function f v) => HasFixity (Formula v p f)
instance (Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Function f v, Variable v, Constants (Predicate p (PTerm v f)), FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v) => Eq (Formula v p f)
instance (Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Function f v, Variable v) => Ord (Formula v p f)
instance (Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Show v, Show p, Show f, HasFixity (Formula v p f), Variable v, Predicate p, Function f v) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f))
instance (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
instance (Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f))
instance (Formula (Formula v p f) (Predicate p (PTerm v f)), Constants (Formula v p f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => Combinable (Formula v p f)
instance (Constants (Formula v p f), Predicate p, Variable v, Function f v) => Constants (Formula v p f)
instance Negatable (Formula v p f)
instance Bijection (Combination (Formula v p f)) (Combination (Formula v p f))
instance Bijection (Formula v p f) (Formula v p f)

module Data.Logic.Types.Harrison.Equal
data FOLEQ
EQUALS :: TermType -> TermType -> FOLEQ
R :: String -> [TermType] -> FOLEQ
data PredName
(:=:) :: PredName
Named :: String -> PredName

-- | Using PredName for the predicate type is not quite appropriate here,
--   but we need to implement this instance so we can use it as a
--   superclass of AtomEq below.
instance Typeable PredName
instance Eq FOLEQ
instance Ord FOLEQ
instance Show FOLEQ
instance Eq PredName
instance Ord PredName
instance Show PredName
instance Data PredName
instance Atom FOLEQ TermType String
instance AtomEq FOLEQ PredName TermType
instance Formula (Formula FOLEQ) FOLEQ => Literal (Formula FOLEQ) FOLEQ
instance HasFixity (Formula FOLEQ)
instance Pretty FOLEQ
instance Formula (Formula FOLEQ) FOLEQ => PropositionalFormula (Formula FOLEQ) FOLEQ
instance Apply FOLEQ PredName TermType
instance Pretty PredName
instance Predicate PredName
instance Constants FOLEQ
instance Constants PredName
instance IsString PredName
instance HasFixity FOLEQ
instance Show (Formula FOLEQ)
instance Arity PredName