Inductive Certificates

We formalize the simple version of Inductive Certificates for unsolvability of automated planning as introduced in [ERH17] and [Eri19]. This file includes :

• the definition of inductive sets and inductive certificates,
• soundness of inductive certificates, and
• completeness of inductive certificates.

Inductive Sets and Inductive Certificates

@[reducible, inline]

abbrev Validator.InductiveSet {n : ℕ} (pt : STRIPS.PlanningTask n) (S : STRIPS.States n) : Prop

A set S is inductive if S[pt.actions] ⊆ S.

Equations

• Validator.InductiveSet pt S = (STRIPS.progression S pt.actions ⊆ S)

@[reducible, inline]

abbrev Validator.InductiveCertificateState {n : ℕ} (pt : STRIPS.PlanningTask n) (s : STRIPS.State n) (S : STRIPS.States n) : Prop

An inductive certificate for a state s is an inductive set containing s which does not contain any goal state.

Equations

• Validator.InductiveCertificateState pt s S = (s ∈ S ∧ (∀ (s : STRIPS.State n), s ∈ S → ¬pt.GoalState s) ∧ Validator.InductiveSet pt S)

@[reducible, inline]

abbrev Validator.InductiveCertificate {n : ℕ} (pt : STRIPS.PlanningTask n) (S : STRIPS.States n) : Prop

An inductive certificate for the a planning task is an inductive certificate for the initial state.

Equations

• Validator.InductiveCertificate pt S = Validator.InductiveCertificateState pt pt.init S

Soundness of Inductive Certificates

theorem Validator.InductiveCertificate.soundness' {n : ℕ} {pt : STRIPS.PlanningTask n} {s : STRIPS.State n} {S : STRIPS.States n} : InductiveCertificateState pt s S → pt.UnsolvableState s

theorem Validator.InductiveCertificate.soundness {n : ℕ} {pt : STRIPS.PlanningTask n} {S : STRIPS.States n} : InductiveCertificate pt S → pt.Unsolvable

Inductive certificates are sound, i.e. if an inductive certificate exists, then the planning problem is unsolvable.

Completeness of Inductive Certificates

theorem Validator.InductiveCertificate.completeness' {n : ℕ} {pt : STRIPS.PlanningTask n} {s : STRIPS.State n} : pt.UnsolvableState s → ∃ (S : STRIPS.States n), InductiveCertificateState pt s S

theorem Validator.InductiveCertificate.completeness {n : ℕ} {pt : STRIPS.PlanningTask n} : pt.Unsolvable → ∃ (S : STRIPS.States n), InductiveCertificate pt S

Inductive certificates are complete, i.e. if a planning problem is unsolvable, then an inductive certificate for the planning problem exists.