FactSet

A FactSet is plainly a Set of Facts.

@[reducible, inline]

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

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

@[simp]

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.

@[simp]

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.

@[simp]

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.mem_constants_iff_mem_terms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {fs : FactSet sig} {c : sig.C} : c ∈ fs.constants ↔ ∃ (t : GroundTerm sig), t ∈ fs.terms ∧ c ∈ t.constants

A constant occurs in the fact set iff it occurs as a constant in one of its terms.

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

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

@[simp]

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.