Eine aufbereitete Darstellung der Quelle

 
     
 
 
Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 
Benutzer

products/Sources/formale Sprachen/C/LibreOffice/icon-themes/breeze_dark_svg/cmd/32/   (LibreOffice Version 25.8.3.2©)  Datei vom 5.10.2025 mit Größe 322 B image not shown  

Bilddatei

prover.sml


products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Verified-Prover/prover.sml

(* To use this file, open OCaml by typing ocaml, and at the prompt type #use "prover.ml";; Formulae are represented using de Bruijn notation: forall x. forall y. P x y is forall. forall. P 1 0 i.e. the variables are numbers indicating how many foralls in the syntax tree you have to jump until you reach the relevant binding forall. Variables are: x_0, x_1, ... They are represented just using their number: 0, 1, ... Predicates are: P_1, P_2, ... and their negations: \overline{P_1}, \overline{P_2}, ... They are represented as follows: P_2(x,y) is PAtom 2 [x,y] and \overline{P_3} [y,z] is NAtom 3 [y,z] N.B. these definitions extracted from thy file by hand, and possibly contain transcription errors. *) open List;; type pred = int;; type var = int;; type form = PAtom of (pred*(var list)) | NAtom of (pred*(var list)) | FConj of form * form | FDisj of form * form | FAll of form | FEx of form ;; let rec preSuc t = match t with [] -> [] | (a::list) -> (match a with 0 -> preSuc list | sucn -> (sucn-1::preSuc list));; let rec fv t = match t with PAtom (p,vs) -> vs | NAtom (p,vs) -> vs | FConj (f,g) -> (fv f)@(fv g) | FDisj (f,g) -> (fv f)@(fv g) | FAll f -> preSuc (fv f) | FEx f -> preSuc (fv f);; let suc x = x+1;; let bump phi y = match y with 0 -> 0 | sucn -> suc (phi (sucn-1));; let rec subst r f = match f with PAtom (p,vs) -> PAtom (p,map r vs) | NAtom (p,vs) -> NAtom (p,map r vs) | FConj (f,g) -> FConj (subst r f, subst r g) | FDisj (f,g) -> FDisj (subst r f, subst r g) | FAll f -> FAll (subst (bump r) f) | FEx f -> FEx (subst (bump r) f);; let finst body w = subst (fun v -> match v with 0 -> w | sucn -> (sucn-1)) body;; let s_of_ns ns = map snd ns;; let sfv s = flatten (map fv s);; let rec maxvar t = match t with [] -> 0 | (a::list) -> max a (maxvar list);; let newvar vs = suc (maxvar vs);; let subs t = match t with [] -> [[]] | (x::xs) -> let (m,f) = x in match f with PAtom (p,vs) -> if mem (NAtom (p,vs)) (map snd xs) then [] else [xs@[(0,PAtom (p,vs))]] | NAtom (p,vs) -> if mem (PAtom (p,vs)) (map snd xs) then [] else [xs@[(0,NAtom (p,vs))]] | FConj (f,g) -> [xs@[(0,f)];xs@[(0,g)]] | FDisj (f,g) -> [xs@[(0,f);(0,g)]] | FAll f -> [xs@[(0,finst f (newvar (sfv (s_of_ns (x::xs)))))]] | FEx f -> [xs@[(0,finst f m);(suc m,FEx f)]];; let rec prove' l = (if l = [] then true else prove' ((fun x -> flatten (map subs x)) l));; let prove s = prove' [s];; let my_f = FDisj ( (FAll (FConj ((NAtom (0,[0])), (NAtom (1,[0])))), (FDisj ((FEx ((PAtom (1,[0])))),(FEx (PAtom (0,[0])))))));; prove [(0,my_f)];;

                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Open Source Software

     Quellcodebibliothek
     Eigene Quellcodes
     Fremde Quellcodes
     Suchen
Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik
Statistik
#Sources=1126438
#Domains=1897691