Database

A Database is a finite set of FunctionFreeFacts.

@[reducible, inline]

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

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, ⋯⟩

@[simp]

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.