Data.Logic.KnowledgeBase

Documentation

data WithId a

Constructors

WithId

Fields

wiItem :: a

wiIdent :: Int

Instances

Eq a => Eq (WithId a)

Data a => Data (WithId a)

Ord a => Ord (WithId a)

Show a => Show (WithId a)

type ProverT inf = StateT (ProverState inf)

A monad for running the knowledge base.

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))

Return the contents of the knowledgebase.

unloadKB :: (Monad m, Ord inf) => SentenceCount -> ProverT inf m (Maybe (KnowledgeBase inf))

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 Bool

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)

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)

Return a flag indicating whether sentence was disproved, along with a disproof.

data ProofResult

Constructors

Disproved

The conjecture is unsatisfiable

Proved

The negated conjecture is unsatisfiable

Invalid

Both are satisfiable

Instances

Eq ProofResult

Data ProofResult

Ord ProofResult

Show ProofResult

SafeCopy ProofResult

data Proof lit

Constructors

Proof

Fields

proofResult :: ProofResult

proof :: Set (ImplicativeForm lit)

Instances

Eq lit => Eq (Proof lit)

(Data lit, Ord lit) => Data (Proof lit)

Ord lit => Ord (Proof lit)

(Ord lit, Show lit, Literal lit atom, FirstOrderFormula lit atom v) => Show (Proof 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)

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)

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.

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

Delete an entry from the KB.

Return a text description of the contents of the knowledgebase.