Certificate

Implementation of the certificates used when validating certificates

inductive Validator.ActionSetExpr : Type

• enum : List ℕ → ActionSetExpr
• union : ℕ → ℕ → ActionSetExpr
• all : ActionSetExpr

def Validator.instReprActionSetExpr.repr : ActionSetExpr → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.instReprActionSetExpr : Repr ActionSetExpr

Equations

• Validator.instReprActionSetExpr = { reprPrec := Validator.instReprActionSetExpr.repr }

@[implicit_reducible]

instance Validator.instToStringActionSetExpr : ToString ActionSetExpr

Equations

• Validator.instToStringActionSetExpr = { toString := Validator.ActionSetExpr.toSting✝ }

inductive Validator.StateSetExpr {n : ℕ} (pt : STRIPS.PlanningTask n) : Type

• empty {n : ℕ} {pt : STRIPS.PlanningTask n} : StateSetExpr pt
• init {n : ℕ} {pt : STRIPS.PlanningTask n} : StateSetExpr pt
• goal {n : ℕ} {pt : STRIPS.PlanningTask n} : StateSetExpr pt
• bdd {n : ℕ} {pt : STRIPS.PlanningTask n} : Formalism.UnprimedVariable pt (BDD (2 * n)) → StateSetExpr pt
• horn {n : ℕ} {pt : STRIPS.PlanningTask n} : Formalism.UnprimedVariable pt (Horn (2 * n)) → StateSetExpr pt
• mods {n : ℕ} {pt : STRIPS.PlanningTask n} : Formalism.UnprimedVariable pt (MODS (2 * n)) → StateSetExpr pt
• neg {n : ℕ} {pt : STRIPS.PlanningTask n} : ℕ → StateSetExpr pt
• inter {n : ℕ} {pt : STRIPS.PlanningTask n} : ℕ → ℕ → StateSetExpr pt
• union {n : ℕ} {pt : STRIPS.PlanningTask n} : ℕ → ℕ → StateSetExpr pt
• progr {n : ℕ} {pt : STRIPS.PlanningTask n} : ℕ → ℕ → StateSetExpr pt
• regr {n : ℕ} {pt : STRIPS.PlanningTask n} : ℕ → ℕ → StateSetExpr pt

@[implicit_reducible]

instance Validator.instToStringStateSetExpr {n : ℕ} {pt : STRIPS.PlanningTask n} : ToString (StateSetExpr pt)

Equations

• Validator.instToStringStateSetExpr = { toString := Validator.StateSetExpr.toString✝ }

inductive Validator.DeadKnowledge : ℕ → Type

• ED (Sᵢ : ℕ) : DeadKnowledge Sᵢ

  Empty set Dead

• UD (Sᵢ a✝ : ℕ) : ℕ → DeadKnowledge Sᵢ

  Union Dead

• SD (Sᵢ a✝ : ℕ) : ℕ → DeadKnowledge Sᵢ

  Subset Dead

• PG (Sᵢ a✝ : ℕ) : ℕ → ℕ → DeadKnowledge Sᵢ

  Progression Goal

• PI (Sᵢ a✝ : ℕ) : ℕ → ℕ → DeadKnowledge Sᵢ

  Progression Initial

• RG (Sᵢ a✝ : ℕ) : ℕ → ℕ → DeadKnowledge Sᵢ

  Regression Goal

• RI (Sᵢ a✝ : ℕ) : ℕ → ℕ → DeadKnowledge Sᵢ

  Regression Initial

def Validator.instReprDeadKnowledge.repr {a✝ : ℕ} : DeadKnowledge a✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.instReprDeadKnowledge {a✝ : ℕ} : Repr (DeadKnowledge a✝)

Equations

• Validator.instReprDeadKnowledge = { reprPrec := Validator.instReprDeadKnowledge.repr }

inductive Validator.StateSubsetKnowledge : ℕ → ℕ → Type

• B1 (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Basic statement 1

• B2 (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Basic statement 2

• B3 (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Basic statement 3

• B4 (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Basic statement 4

• URS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Union Right State

• ULS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Union Left State

• IRS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Intersection Right State

• ILS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Intersection Left State

• DIS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  DIstributivity State

• SUS (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Subset Union State

• SIS (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Subset Intersection State

• STS (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Subset Transitivity State

• AT (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Action Transitivity

• AU (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Action Union

• PT (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Progression Transitivity

• PU (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Progression Union

• PR (Sᵢ S'ᵢ a✝ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Progression to Regression

• RP (Sᵢ S'ᵢ a✝ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Regression to Progression

@[implicit_reducible]

instance Validator.instReprStateSubsetKnowledge {a✝ a✝¹ : ℕ} : Repr (StateSubsetKnowledge a✝ a✝¹)

Equations

• Validator.instReprStateSubsetKnowledge = { reprPrec := Validator.instReprStateSubsetKnowledge.repr }

def Validator.instReprStateSubsetKnowledge.repr {a✝ a✝¹ : ℕ} : StateSubsetKnowledge a✝ a✝¹ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive Validator.ActionSubsetKnowledge : ℕ → ℕ → Type

• B5 (Aᵢ A'ᵢ : ℕ) : ActionSubsetKnowledge Aᵢ A'ᵢ

  Basic statement 5

• URA (Aᵢ A'ᵢ : ℕ) : ActionSubsetKnowledge Aᵢ A'ᵢ

  Union Right Action

• ULA (Aᵢ A'ᵢ : ℕ) : ActionSubsetKnowledge Aᵢ A'ᵢ

  Union Left Action

• SUA (Aᵢ A'ᵢ a✝ : ℕ) : ℕ → ActionSubsetKnowledge Aᵢ A'ᵢ

  Subset Union Action

• STA (Aᵢ A'ᵢ a✝ : ℕ) : ℕ → ActionSubsetKnowledge Aᵢ A'ᵢ

  Subset Transitivity Action

@[implicit_reducible]

instance Validator.instReprActionSubsetKnowledge {a✝ a✝¹ : ℕ} : Repr (ActionSubsetKnowledge a✝ a✝¹)

Equations

• Validator.instReprActionSubsetKnowledge = { reprPrec := Validator.instReprActionSubsetKnowledge.repr }

def Validator.instReprActionSubsetKnowledge.repr {a✝ a✝¹ : ℕ} : ActionSubsetKnowledge a✝ a✝¹ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive Validator.UnsolvableKnowledge : Type

• CI : ℕ → UnsolvableKnowledge

  Conclusion Initial

• CG : ℕ → UnsolvableKnowledge

  Conclusion Goal

def Validator.instReprUnsolvableKnowledge.repr : UnsolvableKnowledge → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.instReprUnsolvableKnowledge : Repr UnsolvableKnowledge

Equations

• Validator.instReprUnsolvableKnowledge = { reprPrec := Validator.instReprUnsolvableKnowledge.repr }

inductive Validator.Knowledge : Type

• dead (Sᵢ : ℕ) : DeadKnowledge Sᵢ → Knowledge
• actionSubset (Aᵢ A'ᵢ : ℕ) : ActionSubsetKnowledge Aᵢ A'ᵢ → Knowledge
• stateSubset (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ → Knowledge
• unsolvable : UnsolvableKnowledge → Knowledge

def Validator.instReprKnowledge.repr : Knowledge → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.instReprKnowledge : Repr Knowledge

Equations

• Validator.instReprKnowledge = { reprPrec := Validator.instReprKnowledge.repr }

@[implicit_reducible]

instance Validator.instToStringKnowledge : ToString Knowledge

Equations

• Validator.instToStringKnowledge = { toString := fun (x : Validator.Knowledge) => "TODO" }

structure Validator.Certificate {n : ℕ} (pt : STRIPS.PlanningTask n) : Type

• actions : Array ActionSetExpr
• states : Array (StateSetExpr pt)
• knowledge : Array Knowledge

@[implicit_reducible]

instance Validator.instToStringCertificate {n : ℕ} {pt : STRIPS.PlanningTask n} : ToString (Certificate pt)

Equations

• One or more equations did not get rendered due to their size.