PDL-Tableaux (Section 4) #
Projections #
Equations
- projection x✝¹ x✝ = (List.map (fun (x : Formula) => formProjection x✝¹ x) x✝).reduceOption
Instances For
Loading and Loaded Histories #
A lpr means we can go k
steps back in the history to
reach an equal node, and all nodes on the way are loaded.
Note: k=0
means the first element of Hist
is the companion.
Equations
- LoadedPathRepeat Hist X = { k : Fin (List.length Hist) // (List.get Hist k).multisetEqTo X ∧ ∀ m ≤ k, (List.get Hist m).isLoaded = true }
Instances For
theorem
LoadedPathRepeat.to_rep
{Hist : History}
{X : Sequent}
(lpr : LoadedPathRepeat Hist X)
:
rep Hist X
instance
instDecidableEqLoadedPathRepeat
{Hist : History}
{X : Sequent}
:
DecidableEq (LoadedPathRepeat Hist X)
def
LoadedPathRepeat.choice
{H : History}
{X : Sequent}
(ne : Nonempty (LoadedPathRepeat H X))
:
LoadedPathRepeat H X
If there is any loaded path repeat, then we can compute one.
FIXME There is probably a more elegant way, avoiding Nonempty
and Fin.find
.
Something like: def getLPR (H : History) (X : Sequent) : Option ... := ...
that might also give us uniqueness of LPRs?
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LoadedPathRepeat_comp_isLoaded
{Hist : History}
{X : Sequent}
(lpr : LoadedPathRepeat Hist X)
:
theorem
LoadedPathRepeat_rep_isLoaded
{Hist : History}
{X : Sequent}
(lpr : LoadedPathRepeat Hist X)
:
instance
instDecidableNonemptyLoadedPathRepeat
{H : History}
{X : Sequent}
:
Decidable (Nonempty (LoadedPathRepeat H X))
Equations
- instDecidableNonemptyLoadedPathRepeat = if h : ∃ (k : Fin (List.length H)), (List.get H k).multisetEqTo X ∧ ∀ m ≤ k, (List.get H m).isLoaded = true then isTrue ⋯ else isFalse ⋯
The PDL rules #
A rule to go from X
to Y
. Note the four variants of the modal rule.
- loadL {L : List Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {R : List Formula} : (~⌈⌈δ⌉⌉⌈α⌉φ) ∈ L → Y = (L.erase (~⌈⌈δ⌉⌉⌈α⌉φ), R, some (Sum.inl (~'⌊⌊δ⌋⌋⌊α⌋AnyFormula.normal φ))) → PdlRule (L, R, none) Y
- loadR {R : List Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {L : List Formula} : (~⌈⌈δ⌉⌉⌈α⌉φ) ∈ R → Y = (L, R.erase (~⌈⌈δ⌉⌉⌈α⌉φ), some (Sum.inr (~'⌊⌊δ⌋⌋⌊α⌋AnyFormula.normal φ))) → PdlRule (L, R, none) Y
- freeL {X : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {L R : List Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} : X = (L, R, some (Sum.inl (~'⌊⌊δ⌋⌋⌊α⌋AnyFormula.normal φ))) → Y = (List.insert (~⌈⌈δ⌉⌉⌈α⌉φ) L, R, none) → PdlRule X Y
- freeR {X : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {L R : List Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} : X = (L, R, some (Sum.inr (~'⌊⌊δ⌋⌋⌊α⌋AnyFormula.normal φ))) → Y = (L, List.insert (~⌈⌈δ⌉⌉⌈α⌉φ) R, none) → PdlRule X Y
- modL {Y : Sequent} {L R : List Formula} {A : ℕ} {X : Sequent} {ξ : AnyFormula} : X = (L, R, some (Sum.inl (~'⌊·A⌋ξ))) → (Y = match ξ with | AnyFormula.normal φ => (~φ :: projection A L, projection A R, none) | AnyFormula.loaded χ => (projection A L, projection A R, some (Sum.inl (~'χ)))) → PdlRule X Y
- modR {Y : Sequent} {L R : List Formula} {A : ℕ} {X : Sequent} {ξ : AnyFormula} : X = (L, R, some (Sum.inr (~'⌊·A⌋ξ))) → (Y = match ξ with | AnyFormula.normal φ => (projection A L, ~φ :: projection A R, none) | AnyFormula.loaded χ => (projection A L, projection A R, some (Sum.inr (~'χ)))) → PdlRule X Y
Instances For
The Tableau [parent, grandparent, ...] child
type.
A closed tableau for X is either of:
- a local tableau for X followed by closed tableaux for all end nodes,
- a PDL rule application
- a successful loaded repeat (MB condition six)
- loc {Hist : History} {X : Sequent} (nrep : ¬rep Hist X) (nbas : ¬X.basic) (lt : LocalTableau X) (next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y) : Tableau Hist X
- pdl {Hist : History} {X Y : Sequent} (nrep : ¬rep Hist X) (bas : X.basic) (r : PdlRule X Y) (next : Tableau (X :: Hist) Y) : Tableau Hist X
- lrep {X : Sequent} {Hist : History} (lpr : LoadedPathRepeat Hist X) : Tableau Hist X
Instances For
Equations
- One or more equations did not get rendered due to their size.
- (Tableau.pdl nrep bas r next).size = 1 + next.size
- (Tableau.lrep lpr).size = 1
Instances For
theorem
Tableau.size_next_lt_of_loc
{a✝ : History}
{a✝¹ : Sequent}
{tab : Tableau a✝ a✝¹}
{nrep : ¬rep a✝ a✝¹}
{nbas : ¬a✝¹.basic}
{lt : LocalTableau a✝¹}
{next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (a✝¹ :: a✝) Y}
(tab_def : tab = loc nrep nbas lt next)
(Y : Sequent)
(Y_in : Y ∈ endNodesOf lt)
:
instance
instDecidableExistsEndNodeOf
{X : Sequent}
{lt : LocalTableau X}
{f : (Y : Sequent) → Y ∈ endNodesOf lt → Prop}
{dec : (Y : Sequent) → (Y_in : Y ∈ endNodesOf lt) → Decidable (f Y Y_in)}
:
Decidable (∃ (Y : Sequent) (Y_in : Y ∈ endNodesOf lt), f Y Y_in)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (Tableau.loc nrep nbas lt next).isLrep = False
- (Tableau.pdl nrep bas r next).isLrep = False
- (Tableau.lrep lpr).isLrep = True
Instances For
A Sequent is inconsistent if there exists a closed tableau for it.
Instances For
A Sequent
is consistent iff it is not inconsistent.
Equations
- consistent x✝ = ¬inconsistent x✝