Atoms, Facts, Rules and the like

In this file, we define the next layers of building blocks above terms. This includes first and foremost Atom and Fact but also Rule, RuleSet, Database and KnowledgeBase to name a few.

The atom-like datastructures are all expressed in terms of a GeneralizedAtom. This will turn out convenient when defining substitutions and homomorphisms next since these can (for the most part) just be defines as generic mapping over GeneralizedAtom.

structure GeneralizedAtom (sig : Signature) (T : Type u) [DecidableEq sig.P] : Type (max u u_1)

A GeneralizedAtom consists of a predicate symbol and a list of terms of an arbitrary type such that the number of terms matches the predicate's arity.

• predicate : sig.P
• terms : List T
• arity_ok : self.terms.length = sig.arity self.predicate

instance instDecidableEqGeneralizedAtom {sig✝ : Signature} {T✝ : Type u_4} {inst✝ : DecidableEq sig✝.P} [DecidableEq T✝] : DecidableEq (GeneralizedAtom sig✝ T✝)

Equations

• instDecidableEqGeneralizedAtom = instDecidableEqGeneralizedAtom.decEq

def instDecidableEqGeneralizedAtom.decEq {sig✝ : Signature} {T✝ : Type u_4} {inst✝ : DecidableEq sig✝.P} [DecidableEq T✝] (x✝ x✝¹ : GeneralizedAtom sig✝ T✝) : Decidable (x✝ = x✝¹)

Equations

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

Atom

@[reducible, inline]

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

An Atom is a GeneralizedAtom with SkolemTerms.

Equations

• Atom sig = GeneralizedAtom sig (SkolemTerm sig)

FunctionFreeAtom

@[reducible, inline]

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

A FunctionFreeAtom is a GeneralizedAtom with VarOrConsts.

Equations

• FunctionFreeAtom sig = GeneralizedAtom sig (VarOrConst sig)

def FunctionFreeAtom.variables {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (a : FunctionFreeAtom sig) : List sig.V

Using VarOrConst.filterVars, we can obtain all variables from the terms of the FunctionFreeAtom.

Equations

• a.variables = VarOrConst.filterVars a.terms

def FunctionFreeAtom.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (a : FunctionFreeAtom sig) : List sig.C

Using VarOrConst.filterConsts, we can obtain all constants from the terms of the FunctionFreeAtom.

Equations

• a.constants = VarOrConst.filterConsts a.terms

def FunctionFreeAtom.skolemize {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (ruleId disjunctIndex : Nat) (frontier : List sig.V) (a : FunctionFreeAtom sig) : Atom sig

We can skolemize a FunctionFreeAtom by skolemizing all its VarOrConsts. This yields an Atom.

Equations

• FunctionFreeAtom.skolemize ruleId disjunctIndex frontier a = { predicate := a.predicate, terms := List.map (VarOrConst.skolemize ruleId disjunctIndex frontier) a.terms, arity_ok := ⋯ }

theorem FunctionFreeAtom.mem_variables {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {a : FunctionFreeAtom sig} {v : sig.V} : v ∈ a.variables ↔ VarOrConst.var v ∈ a.terms

A variable occurs in variables iff it is a term of the `FunctionFreeAtom.

theorem FunctionFreeAtom.mem_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {a : FunctionFreeAtom sig} {c : sig.C} : c ∈ a.constants ↔ VarOrConst.const c ∈ a.terms

A constant occurs in constants iff it is a term of the `FunctionFreeAtom.

theorem FunctionFreeAtom.length_skolemize {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {ruleId disjunctIndex : Nat} {frontier : List sig.V} {a : FunctionFreeAtom sig} : (skolemize ruleId disjunctIndex frontier a).terms.length = a.terms.length

The number of terms remains unchanged when Skolemizing.

theorem FunctionFreeAtom.mem_skolemize_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {ruleId disjunctIndex : Nat} {frontier : List sig.V} {a : FunctionFreeAtom sig} {t : VarOrConst sig} : t ∈ a.terms → VarOrConst.skolemize ruleId disjunctIndex frontier t ∈ (skolemize ruleId disjunctIndex frontier a).terms

If a a VarOrConst occurs in the terms of the FunctionFreeAtom, then the Skolemized VarOrConst occurs in the Skolemized Atom.

FunctionFreeConjunction

@[reducible, inline]

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

A conjunction of FunctionFreeAtoms $p(x, y) \land q(y)$ can simply be represented as a list of FunctionFreeAtoms.

Equations

• FunctionFreeConjunction sig = List (FunctionFreeAtom sig)

def FunctionFreeConjunction.terms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (conj : FunctionFreeConjunction sig) : List (VarOrConst sig)

The terms of a FunctionFreeConjunction are the terms of all its atoms.

Equations

• conj.terms = List.flatMap GeneralizedAtom.terms conj

def FunctionFreeConjunction.vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (conj : FunctionFreeConjunction sig) : List sig.V

The vars of a FunctionFreeConjunction are the variables of all its atoms.

Equations

• conj.vars = List.flatMap FunctionFreeAtom.variables conj

def FunctionFreeConjunction.consts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (conj : FunctionFreeConjunction sig) : List sig.C

The consts of a FunctionFreeConjunction are the constants of all its atoms.

Equations

• conj.consts = List.flatMap FunctionFreeAtom.constants conj

def FunctionFreeConjunction.predicates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (conj : FunctionFreeConjunction sig) : List sig.P

The predicates of a FunctionFreeConjunction are the predicates of all its atoms.

Equations

• conj.predicates = List.map GeneralizedAtom.predicate conj

theorem FunctionFreeConjunction.mem_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {conj : FunctionFreeConjunction sig} {v : sig.V} : v ∈ conj.vars ↔ ∃ (f : FunctionFreeAtom sig), f ∈ conj ∧ VarOrConst.var v ∈ f.terms

Different from the definition, we can also say that a variable is in variables iff there is a FunctionFreeAtom in the conjunction that features the variable as a term.

theorem FunctionFreeConjunction.mem_consts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {conj : FunctionFreeConjunction sig} {c : sig.C} : c ∈ conj.consts ↔ ∃ (f : FunctionFreeAtom sig), f ∈ conj ∧ VarOrConst.const c ∈ f.terms

Different from the definition, we can also say that a constant is in constants iff there is a FunctionFreeAtom in the conjunction that features the constant as a term.

(Disjunctive) (Existential) Rule

A disjunctive existential rule, or simply Rule, formally is an expression of the form $$∀ \vec{x}, \vec{y}. B(x, y) \to \bigvee_{i = 1}^{k} \exists \vec{z}_i. H_i(y_i, z_i)$$ where $B,H_1,\dots,H_k$ are conjunctions of function free atoms, $y$ is exactly the union of all $y_i$ and $x$, $y$, and all $z_i$ are disjoint lists of variables. $y$ is called frontier. $B$ is called body and the $H_i$ are called heads. We call a rule determinstic if $k = 1$ so if the head is merely a conjunction.

To represent this formal definition in Lean, we use a structure with a FunctionFreeConjunction for the body and a list of FunctionFreeConjunctions for the disjunction in the head. For bookkeeping each rule also gets an id. That's it! The frontier variables can simply be defined as the variables occurring both in body and head and the existential variables can be indentified as the variables that occur only in the head, without the need for explicit quantification.

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

The definition of a Rule as discussed above.

• id : Nat
• body : FunctionFreeConjunction sig
• head : List (FunctionFreeConjunction sig)

instance instDecidableEqRule {sig✝ : Signature} {inst✝ : DecidableEq sig✝.P} {inst✝¹ : DecidableEq sig✝.C} {inst✝² : DecidableEq sig✝.V} : DecidableEq (Rule sig✝)

Equations

• instDecidableEqRule = instDecidableEqRule.decEq

def instDecidableEqRule.decEq {sig✝ : Signature} {inst✝ : DecidableEq sig✝.P} {inst✝¹ : DecidableEq sig✝.C} {inst✝² : DecidableEq sig✝.V} (x✝ x✝¹ : Rule sig✝) : Decidable (x✝ = x✝¹)

Equations

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

def Rule.frontier_for_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) (i : Fin r.head.length) : List sig.V

This function returns the frontier variables that occur in a given head disjunct. This is a sublist of all the frontier variables.

Equations

• r.frontier_for_head i = List.filter (fun (v : sig.V) => decide (v ∈ r.head[↑i].vars)) r.body.vars

def Rule.frontier {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.V

This returns all the frontier variables of the rule, i.e. the variables that occur in both body and some head.

Equations

• r.frontier = List.filter (fun (v : sig.V) => r.head.any fun (h : FunctionFreeConjunction sig) => decide (v ∈ h.vars)) r.body.vars

def Rule.pure_body_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.V

The pure_body_vars are the variables from the body that are not in the frontier.

Equations

• r.pure_body_vars = List.filter (fun (x : sig.V) => decide ¬x ∈ r.frontier) r.body.vars

def Rule.isDatalog {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : Bool

We call a rule isDatalog if it does not contain existential variables, i.e. if all head variables occur in the body.

Equations

• r.isDatalog = r.head.all fun (h : FunctionFreeConjunction sig) => h.vars.all fun (v : sig.V) => decide (v ∈ r.body.vars)

def Rule.isDeterministic {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : Bool

We call a rule isDeterministic if it has exactly one head disjunct.

Equations

• r.isDeterministic = decide (r.head.length = 1)

def Rule.predicates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.P

The predicate symbols of a rule are just the predicate symbols from the body and all heads.

Equations

• r.predicates = r.body.predicates ++ List.flatMap FunctionFreeConjunction.predicates r.head

def Rule.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.C

The constants of a rule are just the constants from the body and all heads.

Equations

• r.constants = r.body.consts ++ List.flatMap (fun (conj : FunctionFreeConjunction sig) => conj.consts) r.head

def Rule.head_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List sig.C

Sometimes we require only the constants from the heads and therefore we define them here.

Equations

• r.head_constants = List.flatMap (fun (conj : FunctionFreeConjunction sig) => conj.consts) r.head

def Rule.existential_vars_for_head_disjunct {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) (i : Nat) (lt : i < r.head.length) : List sig.V

The existential variables for a given head are simply the variables from the head that are not in the frontier.

Equations

• r.existential_vars_for_head_disjunct i lt = List.filter (fun (v : sig.V) => decide ¬v ∈ r.frontier) r.head[i].vars

def Rule.skolem_functions {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : List (SkolemFS sig)

The Skolem function symbols of a rule are all SkolemFS with the rule id, all possible head indices and the respective existential variables.

Equations

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

theorem Rule.mem_frontier_iff_mem_frontier_for_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {v : sig.V} : v ∈ r.frontier ↔ ∃ (i : Fin r.head.length), v ∈ r.frontier_for_head i

A variable is a frontier variable if and only if it is a frontier variable in some head disjunct.

theorem Rule.mem_frontier_for_head_of_mem_frontier_of_mem_head_terms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {v : sig.V} {i : Fin r.head.length} : v ∈ r.frontier → VarOrConst.var v ∈ r.head[↑i].terms → v ∈ r.frontier_for_head i

A variable is in the frontier of a head if it is in the frontier of the rule and occurs as a term in the given head.

theorem Rule.frontier_subset_vars_body {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} : r.frontier ⊆ r.body.vars

All frontier variables occur in the body.

theorem Rule.frontier_for_head_subset_vars_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {r : Rule sig} {i : Nat} {lt : i < r.head.length} : r.frontier_for_head ⟨i, lt⟩ ⊆ r.head[i].vars

The frontier variables in a given head occur in the list of variables for the same head.

theorem Rule.head_constants_subset_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) : r.head_constants ⊆ r.constants

The head constants of the rule are also constants of the whole rule.

RuleSet and RuleList

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

A RuleSet is a Set (Rule sig) where rules are uniquely identified by their id.

• rules : Set (Rule sig)
• id_unique (r1 r2 : Rule sig) : r1 ∈ self.rules ∧ r2 ∈ self.rules ∧ r1.id = r2.id → r1 = r2

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

A RuleList is a List (Rule sig) where rules are uniquely identified by their id.

• rules : List (Rule sig)
• id_unique (r1 r2 : Rule sig) : r1 ∈ self.rules ∧ r2 ∈ self.rules ∧ r1.id = r2.id → r1 = r2

RuleSet

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

A RuleSet is is deterministic if each rule is.

Equations

• rs.isDeterministic = ∀ (r : Rule sig), r ∈ rs.rules → r.isDeterministic = true

def RuleSet.predicates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : Set sig.P

The predicate symbols of a RuleSet are the predicate symbols from all rules.

Equations

• rs.predicates p = ∃ (r : Rule sig), r ∈ rs.rules ∧ p ∈ r.predicates

def RuleSet.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : Set sig.C

The constants of a RuleSet are the constants from all rules.

Equations

• rs.constants c = ∃ (r : Rule sig), r ∈ rs.rules ∧ c ∈ r.constants

def RuleSet.head_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : Set sig.C

The head constants of a RuleSet are the head constants from all rules.

Equations

• rs.head_constants c = ∃ (r : Rule sig), r ∈ rs.rules ∧ c ∈ r.head_constants

def RuleSet.skolem_functions {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : Set (SkolemFS sig)

The Skolem function symbols of a RuleSet are the Skolem function symbols from all rules.

Equations

• rs.skolem_functions f = ∃ (r : Rule sig), r ∈ rs.rules ∧ f ∈ r.skolem_functions

theorem RuleSet.predicates_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : rs.rules.finite → rs.predicates.finite

If the RuleSet is finite, so are the predicates.

theorem RuleSet.constants_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : rs.rules.finite → rs.constants.finite

If the RuleSet is finite, so are the constants.

theorem RuleSet.head_constants_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : rs.rules.finite → rs.head_constants.finite

If the RuleSet is finite, so are the head_constants.

theorem RuleSet.skolem_functions_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : rs.rules.finite → rs.skolem_functions.finite

If the RuleSet is finite, so are the skolem_functions.

theorem RuleSet.head_constants_subset_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : rs.head_constants ⊆ rs.constants

The head_constants of a RuleSet are a subset of the constants.

RuleList

def RuleList.get_by_id {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (id : Nat) (id_mem : ∃ (r : Rule sig), r ∈ rl.rules ∧ r.id = id) : Rule sig

In a RuleList, we can obtain a rule based on its id.

Equations

• rl.get_by_id id id_mem = (List.find? (fun (r : Rule sig) => decide (r.id = id)) rl.rules).get ⋯

theorem RuleList.get_by_id_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (id : Nat) (id_mem : ∃ (r : Rule sig), r ∈ rl.rules ∧ r.id = id) : rl.get_by_id id id_mem ∈ rl.rules

A rule that we get by id is in the RuleList.

theorem RuleList.get_by_id_self {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (r : Rule sig) (mem : r ∈ rl.rules) : rl.get_by_id r.id ⋯ = r

A rule that we get by id is indeed the rule that the id belongs to.

Facts and FunctionFreeFacts

@[reducible, inline]

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

A Fact is a GeneralizedAtom with GroundTerms.

Equations

• Fact sig = GeneralizedAtom sig (GroundTerm sig)

@[reducible, inline]

abbrev FunctionFreeFact (sig : Signature) [DecidableEq sig.P] : Type (max u_3 u_1)

A FunctionFreeFact is a GeneralizedAtom with constants.

Equations

• FunctionFreeFact sig = GeneralizedAtom sig sig.C

def Fact.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) : List sig.C

The constants of a Fact are the constants of all terms.

Equations

• f.constants = List.flatMap GroundTerm.constants f.terms

def Fact.function_symbols {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) : List (SkolemFS sig)

The function_symbols of a Fact are the function symbols of all terms.

Equations

• f.function_symbols = List.flatMap GroundTerm.functions f.terms

def Fact.isFunctionFree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) : Prop

A Fact is function free, if each term is a constant.

Equations

• f.isFunctionFree = ∀ (t : GroundTerm sig), t ∈ f.terms → ∃ (c : sig.C), t = GroundTerm.const c

def Fact.toFunctionFreeFact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) (isFunctionFree : f.isFunctionFree) : FunctionFreeFact sig

If a Fact isFunctionFree, then we can convert it to a FunctionFreeFact.

Equations

• f.toFunctionFreeFact isFunctionFree = { predicate := f.predicate, terms := List.map (fun (t : { x : GroundTerm sig // x ∈ f.terms }) => t.val.toConst ⋯) f.terms.attach, arity_ok := ⋯ }

def FunctionFreeFact.toFact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : FunctionFreeFact sig) : Fact sig

A FunctionFreeFact can always be converted to a Fact.

Equations

• f.toFact = { predicate := f.predicate, terms := List.map GroundTerm.const f.terms, arity_ok := ⋯ }

theorem FunctionFreeFact.toFact_isFunctionFree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : FunctionFreeFact sig) : f.toFact.isFunctionFree

A Fact obtained from a FunctionFreeFact isFunctionFree.

theorem FunctionFreeFact.toFunctionFreeFact_after_toFact_is_id {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : FunctionFreeFact sig) : f.toFact.toFunctionFreeFact ⋯ = f

Converting a FunctionFreeFact to a Fact and back yields the initial FunctionFreeFact.

theorem Fact.toFact_after_toFunctionFreeFact_is_id {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) (isFunctionFree : f.isFunctionFree) : (f.toFunctionFreeFact isFunctionFree).toFact = f

Converting a Fact to a FunctionFreeFact and back yields the initial Fact.

FactSet

@[reducible, inline]

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

A FactSet is plainly a Set of Facts.

Equations

• FactSet sig = Set (Fact sig)

def FactSet.predicates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) : Set sig.P

The predicate symbols of a FactSet are the predicate symbols from all facts.

Equations

• fs.predicates p = ∃ (f : Fact sig), f ∈ fs ∧ f.predicate = p

def FactSet.terms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) : Set (GroundTerm sig)

The terms of a FactSet are the terms from all facts.

Equations

• fs.terms t = ∃ (f : Fact sig), f ∈ fs ∧ t ∈ f.terms

def FactSet.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) : Set sig.C

The constants of a FactSet are the constants from all facts.

Equations

• fs.constants c = ∃ (f : Fact sig), f ∈ fs ∧ c ∈ f.constants

def FactSet.function_symbols {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) : Set (SkolemFS sig)

The function symbols of a FactSet are the function symbols from all facts.

Equations

• fs.function_symbols func = ∃ (f : Fact sig), f ∈ fs ∧ func ∈ f.function_symbols

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

A FactSet is function free if all of its facts are.

Equations

• fs.isFunctionFree = ∀ (f : Fact sig), f ∈ fs → f.isFunctionFree

theorem FactSet.mem_terms_toSet {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {l : List (Fact sig)} (t : GroundTerm sig) : t ∈ terms l.toSet ↔ t ∈ List.flatMap GeneralizedAtom.terms l

When converting a list to a FactSet, the terms remain the same.

theorem FactSet.terms_subset_of_subset {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {fs1 fs2 : FactSet sig} : fs1 ⊆ fs2 → fs1.terms ⊆ fs2.terms

The a FactSet is a subset of another, then their terms share this subset relation.

theorem FactSet.terms_union {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {fs1 fs2 : FactSet sig} : (fs1 ∪ fs2).terms = fs1.terms ∪ fs2.terms

The terms of the union of two FactSets are the union of the terms of both sets.

theorem FactSet.terms_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (finite : Set.finite fs) : fs.terms.finite

If a FactSet is finite, so are its terms.

theorem FactSet.mem_constants_toSet {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {l : List (Fact sig)} (c : sig.C) : c ∈ constants l.toSet ↔ c ∈ List.flatMap Fact.constants l

When converting a list to a FactSet, the constants remain the same.

theorem FactSet.constants_union {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {fs1 fs2 : FactSet sig} : (fs1 ∪ fs2).constants = fs1.constants ∪ fs2.constants

The constants of the union of two FactSets are the union of the constants of both sets.

theorem FactSet.constants_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (fin : Set.finite fs) : fs.constants.finite

If a FactSet is finite, so are its constants.

theorem FactSet.finite_of_preds_finite_of_terms_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) : fs.predicates.finite → fs.terms.finite → Set.finite fs

A FactSet is finite if both its predicates and terms are. This holds since the fact set must be a subset of all facts that can possibly be constructed using the prediactes and terms available. This overapproximation is easily shown to be finite.

theorem FactSet.list_of_facts_for_list_of_terms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {ts : List (GroundTerm sig)} {fs : FactSet sig} (ts_sub : ts.toSet ⊆ fs.terms) : ∃ (l : List (Fact sig)), l.toSet ⊆ fs ∧ ts ⊆ List.flatMap GeneralizedAtom.terms l

For a list of terms in a given FactSet, we can find a list of facts in the fact set such that all the terms from the list occur in the list of facts.

Database

@[reducible, inline]

abbrev Database (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max 0 u_3 u_1)

A Database is a finite set of FunctionFreeFacts.

Equations

• Database sig = { X : Set (FunctionFreeFact sig) // X.finite }

def Database.toFactSet {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (db : Database sig) : { fs : FactSet sig // Set.finite fs ∧ fs.isFunctionFree }

Any Database can trivially be converted to a finite and function free FactSet.

Equations

• db.toFactSet = ⟨fun (f : Fact sig) => ∃ (f' : FunctionFreeFact sig), f' ∈ db.val ∧ f'.toFact = f, ⋯⟩

def Database.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (db : Database sig) : { C : Set sig.C // C.finite }

Each Database has a finite set of constants.

Equations

• db.constants = ⟨fun (c : sig.C) => ∃ (f : FunctionFreeFact sig), f ∈ db.val ∧ c ∈ f.terms, ⋯⟩

theorem Database.toFactSet_constants_same {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (db : Database sig) : db.toFactSet.val.constants = db.constants.val

When converting a Database to a FactSet, the constants remain the same.

KnowledgeBase

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

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.

• 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