Atoms, Facts, Rules and the like

In this directory, we define the next layers of building blocks above terms. This includes first and foremost FunctionFreeAtom 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

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.

@[instance_reducible]

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

Equations

• instDecidableEqGeneralizedAtom = instDecidableEqGeneralizedAtom.decEq

theorem GeneralizedAtom.length_terms_eq_of_predicate_eq {sig : Signature} {T : Type u} [DecidableEq sig.P] {a b : GeneralizedAtom sig T} : a.predicate = b.predicate → a.terms.length = b.terms.length

If two atoms have the same predicate, then they thave an equal number of terms