diff options
Diffstat (limited to 'semestr-3/pf/lista5/proof/proof.mli')
-rw-r--r-- | semestr-3/pf/lista5/proof/proof.mli | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/semestr-3/pf/lista5/proof/proof.mli b/semestr-3/pf/lista5/proof/proof.mli new file mode 100644 index 0000000..2c939fd --- /dev/null +++ b/semestr-3/pf/lista5/proof/proof.mli @@ -0,0 +1,85 @@ +open Logic + +type context = (string * formula) list +type goalDesc = context * formula + +type proof +type goal + +(** Zamienia ukończony dowód na twierdzenie *) +val qed : proof -> theorem + +(** Zwraca liczbę pozostałych w dowodze celów (0 <-> dowód jest gotowy i można go zakończyć) *) +val numGoals : proof -> int + +(** Zwraca listę celów w danym dowodzie *) +val goals : proof -> goalDesc list + +(** Tworzy pusty dowód podanego twierdzenia *) +val proof : context -> formula -> proof + +(** Zwraca (assm, phi), gdzie assm oraz phi to odpowiednio dostępne + założenia oraz formuła do udowodnienia w aktywnym podcelu *) +val goal : goal -> goalDesc + +(** Ustawia aktywny cel w danym dowodzie *) +val focus : int -> proof -> goal + +(** Zapomina informację o celu *) +val unfocus : goal -> proof + +(** Zmienia (cyklicznie) aktywny cel na następny/poprzedni *) +val next : goal -> goal +val prev : goal -> goal + +(** Wywołanie intro name pf odpowiada regule wprowadzania implikacji. + To znaczy aktywna dziura wypełniana jest regułą: + + (nowy aktywny cel) + (name,ψ) :: Γ ⊢ φ + -----------------(→I) + Γ ⊢ ψ → φ + + Jeśli aktywny cel nie jest implikacją, wywołanie kończy się błędem *) +val intro : string -> goal -> goal + +(** Wywołanie apply ψ₀ pf odpowiada jednocześnie eliminacji implikacji + i eliminacji fałszu. Tzn. jeśli do udowodnienia jest φ, a ψ₀ jest + postaci ψ₁ → ... → ψn → φ to aktywna dziura wypełniana jest regułami + + (nowy aktywny cel) (nowy cel) + Γ ⊢ ψ₀ Γ ⊢ ψ₁ + ----------------------(→E) (nowy cel) + ... Γ ⊢ ψn + ----------------------------(→E) + Γ ⊢ φ + + Natomiast jeśli ψ₀ jest postaci ψ₁ → ... → ψn → ⊥ to aktywna dziura + wypełniana jest regułami + + (nowy aktywny cel) (nowy cel) + Γ ⊢ ψ₀ Γ ⊢ ψ₁ + ----------------------(→E) (nowy cel) + ... Γ ⊢ ψn + ----------------------------(→E) + Γ ⊢ ⊥ + -----(⊥E) + Γ ⊢ φ *) +val apply : formula -> goal -> goal + +(** Wywołanie `apply_thm thm pf` działa podobnie do + `apply (Logic.consequence thm) pf`, tyle że aktywna dziura od razu + jest wypełniana dowodem thm, a otrzymane drzewo nie jest + sfokusowane na żadnym z celów. +*) + +val apply_thm : theorem -> goal -> proof + +(** Wywołanie `apply_assm name pf` działa tak jak + `apply (Logic.by_assumption f) pf`, gdzie f jest założeniem o + nazwie name +*) +val apply_assm : string -> goal -> proof + +val pp_print_proof : Format.formatter -> proof -> unit +val pp_print_goal : Format.formatter -> goal -> unit |