Models

FactSets can model rules, databases and knowledge bases in a first order logic sense. Here, we briefly define what this formally means in terms of our definitions.

def FactSet.modelsDb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (db : Database sig) : Prop

A FactSet models a Database if the database is a subset of the fact set.

Equations

• fs.modelsDb db = (db.toFactSet.val ⊆ fs)

def FactSet.modelsRule {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (rule : Rule sig) : Prop

A FactSet models a Rule if each substitution that matches the rule body in the fact set can be existended to a substitution for some head of the rule such that this mapped head is already contained in the fact set. The extension of the substitution intuitivly tries to find a suitable mapping for the existential variables that show that the rule is already satisfied (under FOL semantics).

Equations

• One or more equations did not get rendered due to their size.

def FactSet.modelsRules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (rules : RuleSet sig) : Prop

A FactSet models a RuleSet if it models each rule.

Equations

• fs.modelsRules rules = ∀ (r : Rule sig), r ∈ rules.rules → fs.modelsRule r

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

A FactSet models a KnowledgeBase if it models both the database and the rule set.

Equations

• fs.modelsKb kb = (fs.modelsDb kb.db ∧ fs.modelsRules kb.rules)

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

A FactSet $F$ universally models a KnowledgeBase if it models the knowledge base but also, for each model $M$ of the knowledge base, we can find a homomorphism from $F$ into $M$. Intuitively, universal models are the most general models (but not necessarily the smallest ones).

Equations

• fs.universallyModelsKb kb = (fs.modelsKb kb ∧ ∀ (m : FactSet sig), m.modelsKb kb → ∃ (h : GroundTermMapping sig), h.isHomomorphism fs m)