logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Data.Logic.KnowledgeBase

Synopsis

Documentation

data WithId a Source

Constructors

 WithId FieldswiItem :: a wiIdent :: Int

Instances

 Typeable1 WithId Eq a => Eq (WithId a) (Typeable (WithId a), Data a) => Data (WithId a) (Eq (WithId a), Ord a) => Ord (WithId a) Show a => Show (WithId a)

type ProverT inf = StateT (ProverState inf)Source

A monad for running the knowledge base.

runProver' :: Maybe Int -> ProverT' v term inf Identity a -> aSource

runProverT' :: Monad m => Maybe Int -> ProverT' v term inf m a -> m aSource

getKB :: Monad m => ProverT inf m (Set (WithId inf))Source

Return the contents of the knowledgebase.

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.

Constructors

 Disproved The conjecture is unsatisfiable Proved The negated conjecture is unsatisfiable Invalid Both are satisfiable

data Proof lit Source

Constructors

 Proof FieldsproofResult :: ProofResult proof :: Set (ImplicativeForm lit)

Instances

 Typeable1 Proof Eq lit => Eq (Proof lit) (Typeable (Proof lit), Data lit, Ord lit) => Data (Proof lit) (Eq (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)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.

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]Source

showKB :: (Show inf, Monad m) => ProverT inf m StringSource

Delete an entry from the KB.

Return a text description of the contents of the knowledgebase.