KnowledgeBase

A KnowledgeBase is a pair of a Database and a RuleSet. Note that usually the RuleSet is enforced to be finite but we only restrict this in places where we really need this.

structure KnowledgeBase (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max (max u_1 u_2) u_3)

• db : Database sig
• rules : RuleSet sig

def KnowledgeBase.isDeterministic {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (kb : KnowledgeBase sig) : Prop

A KnowledgeBase is determinstic if the underlying RuleSet is.

Equations

• kb.isDeterministic = kb.rules.isDeterministic