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.