octalgo.datalogcert.completeness

The DatalogCert Library CNRS & Université Paris-Sud, Université Paris-Saclay Copyright 2016-2019 : FormalData Original authors: Véronique Benzaken Évelyne Contejean Stefania Dumbrava
Eigth and last part of the original file "pengine.v" with modifications


Require Import syntax.
Require Import subs.
Require Import pmatch.
Require Import bSemantics.
Require Import monotonicity.
Require Import soundness.
Require Import fixpoint.

Set Implicit Arguments.

Section Completeness.

Completeness

Variable n : nat.
default constant
Variable def : syntax.constant.
program
Variable p : program.
p is safe
Hypothesis p_safe : prog_safe p.
the set of ground atoms
Definition bp : {set gatom} := setT.

Proof that B(P) is a model of the safe program p.
Lemma bpM : prog_true p bp.

There is a set of ground atoms, shuch that it is an iteration of fwd_chain from the empty set, it is a model of p and it is the smallest one
Lemma fwd_chain_complete :
{ m : {set gatom} &
{ n : nat | [/\ prog_true p m
              , m = iter n (fwd_chain def p) set0
              & ∀ m', prog_true p m' → m \subset m']}}.

Forward Chain Completeness:

Let p be a safe program. The iterative forward chain inference engine terminates (after iterating as many times as there are elements in B(P)) and outputs a minimal model for p.
Lemma incr_fwd_chain_complete (s0 : {set gatom}) :
{ m : {set gatom} &
{ n : nat | [/\ prog_true p m
              , n = #|bp|
              , m = iter n (fwd_chain def p) s0
              & ∀ (m' : {set gatom}), s0 \subset m' → prog_true p m' → m \subset m']}}.

End Completeness.