Niezawodne programowanie
alt-ergo
Dowodzenie twierdzeń
26/06/13 17:58
GNATprove używa domyślnie programu alt-ergo do dowodzenia poprawności programu.
Pliki z twierdzeniami do udowodnienia mają prostą składnię.
Przykład 1
W pliku test1.why wpisano:
logic p, q: prop
axiom a1: p and q
goal g: p
Zdefiniowano w nim dwie zmienne zdaniowe p i q oraz aksjomat p and q.
Zadano również cel do udowodnienia w postaci formuły p.
Poniżej pokazano sposób uruchomienia programu alt-ergo dla pliku test1.why:
$ alt-ergo test1.why
File "test1.why", line 5, characters 1-10:Valid (0.0132) (0)
Jak widać została wykazana prawdziwość celu (wykazano wynikanie celu g z aksjomatu a1).
Przykład 2
W pliku test2.why wpisano:
logic p, q: prop
axiom a2: p or q
goal g: p
Tym razem aksjomat ma postać p or q.
Po uruchomieniu programu alt-ergo:
$ alt-ergo test2.why
File "test2.why", line 5, characters 1-10:I don't know
przekonamy się, że nie był on w stanie wyprowadzić celu g z aksjomatu a2.
Przykład 3
Ciekawą własnością programu alt-ergo jest ta, że gdy uda mu się udowodnić cel, to powiada Valid a w każdym innym przypadku, odpowiada I don’t know (nawet wtedy gdy cel w oczywisty sposób nie wynika z aksjomatów).
W pliku test3.why wpisano:
goal g: false
Oczywiście, fałszywy cel nie jest możliwy do udowodnienia, jednak program alt-ergo odpowiada z rozbrajającą szczerością:
$ alt-ergo test3.why
File "test3.why", line 1, characters 1-14:I don't know
Przykład 4
Rozpatrzmy klasyczny przykład z logiki pierwszego rzędu. Zdefiniujemy dziedzinę domain, dwa predykaty man i mortal oraz dwie stałe w dziedzinie socrates i zeus:
type domain
logic man : domain -> prop
logic mortal : domain -> prop
logic socrates : domain
logic zeus : domain
Przyjmiemy dwa aksjomaty:
Zapiszemy je następująco:
axiom A1: man(socrates)
axiom A2: forall x : domain. man(x) -> mortal(x)
Na koniec zadamy dwa cele do udowodnienia:
Co zapisujemy następująco:
goal G1: mortal(socrates)
goal G2: mortal(zeus)
Wszystko umieścimy w pliku test4.why.
Kiedy uruchomimy program alt-ergo otrzymamy następujące odpowiedzi:
$ alt-ergo test4.why
File "test4.why", line 15, characters 1-26:Valid (0.0117) (0)
File "test4.why", line 17, characters 1-22:I don't know
Jak widać pierwszy cel mortal(socrates) został udowodniony, natomiast program alt-ergo nie był w stanie udowodnić drugi cel mortal(zeus).
Udostępnione pliki:
Więcej przykładów na stronie programu alt-ergo:
Pliki z twierdzeniami do udowodnienia mają prostą składnię.
Przykład 1
W pliku test1.why wpisano:
logic p, q: prop
axiom a1: p and q
goal g: p
Zdefiniowano w nim dwie zmienne zdaniowe p i q oraz aksjomat p and q.
Zadano również cel do udowodnienia w postaci formuły p.
Poniżej pokazano sposób uruchomienia programu alt-ergo dla pliku test1.why:
$ alt-ergo test1.why
File "test1.why", line 5, characters 1-10:Valid (0.0132) (0)
Jak widać została wykazana prawdziwość celu (wykazano wynikanie celu g z aksjomatu a1).
Przykład 2
W pliku test2.why wpisano:
logic p, q: prop
axiom a2: p or q
goal g: p
Tym razem aksjomat ma postać p or q.
Po uruchomieniu programu alt-ergo:
$ alt-ergo test2.why
File "test2.why", line 5, characters 1-10:I don't know
przekonamy się, że nie był on w stanie wyprowadzić celu g z aksjomatu a2.
Przykład 3
Ciekawą własnością programu alt-ergo jest ta, że gdy uda mu się udowodnić cel, to powiada Valid a w każdym innym przypadku, odpowiada I don’t know (nawet wtedy gdy cel w oczywisty sposób nie wynika z aksjomatów).
W pliku test3.why wpisano:
goal g: false
Oczywiście, fałszywy cel nie jest możliwy do udowodnienia, jednak program alt-ergo odpowiada z rozbrajającą szczerością:
$ alt-ergo test3.why
File "test3.why", line 1, characters 1-14:I don't know
Przykład 4
Rozpatrzmy klasyczny przykład z logiki pierwszego rzędu. Zdefiniujemy dziedzinę domain, dwa predykaty man i mortal oraz dwie stałe w dziedzinie socrates i zeus:
type domain
logic man : domain -> prop
logic mortal : domain -> prop
logic socrates : domain
logic zeus : domain
Przyjmiemy dwa aksjomaty:
- A1: Socrates jest człowiekiem.
- A2: Każdy człowiek jest śmiertelny.
Zapiszemy je następująco:
axiom A1: man(socrates)
axiom A2: forall x : domain. man(x) -> mortal(x)
Na koniec zadamy dwa cele do udowodnienia:
- G1: Sokrates jest śmiertelny.
- G2: Zeus jest śmiertelny.
Co zapisujemy następująco:
goal G1: mortal(socrates)
goal G2: mortal(zeus)
Wszystko umieścimy w pliku test4.why.
Kiedy uruchomimy program alt-ergo otrzymamy następujące odpowiedzi:
$ alt-ergo test4.why
File "test4.why", line 15, characters 1-26:Valid (0.0117) (0)
File "test4.why", line 17, characters 1-22:I don't know
Jak widać pierwszy cel mortal(socrates) został udowodniony, natomiast program alt-ergo nie był w stanie udowodnić drugi cel mortal(zeus).
Udostępnione pliki:
- test1.why
- test2.why
- test3.why
- test4.why
- alt-ergo.zip archiwum zawierające powyższe pliki
Więcej przykładów na stronie programu alt-ergo: