Universality of the Core Chase Result

Just as for RegularChaseTrees, the result of a CoreChaseTree is a universal model set of the underlying KnowledgeBase. Also, for determistic CoreChaseBranches, result is a universal model.

theorem CoreChaseTree.universal_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} (ct : CoreChaseTree kb) (terminates : ct.terminates) (m : FactSet sig) : m.modelsKb kb → ∃ (fs : FactSet sig), ∃ (h : GroundTermMapping sig), fs ∈ CoreTreeDerivation.result ct.toTreeDerivation terminates ∧ h.isHomomorphism fs m

def CoreTreeDerivation.firstResult {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} (td : CoreTreeDerivation rules) (terminates : TreeDerivation.terminates td) : FactSet sig

The firstResult is the result of the firstBranch.

Equations

• td.firstResult terminates = CoreChaseDerivation.result (TreeDerivation.firstBranch td) ⋯

theorem CoreTreeDerivation.firstResult_mem_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} {terminates : TreeDerivation.terminates td} : td.firstResult terminates ∈ td.result terminates

The firstResult is a member of the TreeDerivation.result.

theorem CoreChaseTree.deterministicChaseTreeResultUniversallyModelsKb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {ct : CoreChaseTree kb} (det : kb.isDeterministic) (terminates : ct.terminates) : (CoreTreeDerivation.firstResult ct.toTreeDerivation terminates).universallyModelsKb kb

In the deterministic setting, the firstResult of a CoreChaseTree is by itself a universal model.

theorem CoreChaseDerivation.firstResult_intoTree_eq_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} (cd : CoreChaseDerivation rules) (det : rules.isDeterministic) (terminates : ChaseDerivation.terminates cd) : CoreTreeDerivation.firstResult (ChaseDerivation.intoTree cd det) ⋯ = cd.result terminates

The firstResult of intoTree is the original ChaseDerivationSkeleton.result.

theorem CoreChaseBranch.result_universallyModels_kb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} (det : kb.isDeterministic) (terminates : cb.terminates) : (CoreChaseDerivation.result cb.toChaseDerivation terminates).universallyModelsKb kb