Safe Haskell  None 

 data WithId a = WithId {}
 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
 getKB :: Monad m => ProverT inf m (Set (WithId inf))
 unloadKB :: (Monad m, Ord inf) => SentenceCount > ProverT inf m (Maybe (KnowledgeBase inf))
 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
 theoremKB :: forall m formula atom term v p f lit. (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)
 inconsistantKB :: forall m formula atom term v p f lit. (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
 data Proof lit = Proof {
 proofResult :: ProofResult
 proof :: Set (ImplicativeForm lit)
 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)
 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]
 showKB :: (Show inf, Monad m) => ProverT inf m String
Documentation
runProver' :: Maybe Int > ProverT' v term inf Identity a > aSource
runProverT' :: Monad m => Maybe Int > ProverT' v term inf m a > m aSource
unloadKB :: (Monad m, Ord inf) => SentenceCount > ProverT inf m (Maybe (KnowledgeBase inf))Source
Remove a particular sentence from the knowledge base
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 BoolSource
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.
theoremKB :: forall m formula atom term v p f lit. (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)Source
Return a flag indicating whether sentence was proved, along with a proof.
inconsistantKB :: forall m formula atom term v p f lit. (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)Source
Return a flag indicating whether sentence was disproved, along with a disproof.
data ProofResult Source
Proof  

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)Source
See whether the sentence is true, false or invalid. Return proofs for truth and falsity.
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)Source
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.