skype transcript

[Dimitrios Vytiniotis]

[13:14:28] Dimitrios Vytiniotis: Hi Koen are you tehre?
[13:21:32] Koen Claessen: yes
[13:21:39] Dimitrios Vytiniotis: shall we checkpoint briefly?
[13:21:43] Koen Claessen: ok
[13:21:49] Koen Claessen: is simon not there?
[13:21:52] Dimitrios Vytiniotis: no
[13:21:54] Koen Claessen: ah ok
[13:21:55] Dimitrios Vytiniotis: he is travelling
[13:21:58] Koen Claessen: I was chatting with him
[13:22:06] Koen Claessen: and did not see your chat
[13:22:11] Koen Claessen: next time, just call me on Skype
[13:22:12] Dimitrios Vytiniotis: ok
[13:22:18] Koen Claessen: I only have Skype on when I am making a call
[13:22:23] *** Call to Koen Claessen, duration 00:28. ***
[13:22:58] *** Call to Koen Claessen ***
[13:24:13] Dimitrios Vytiniotis: lem :: CF -> { .... } && CF
[13:24:45] Dimitrios Vytiniotis: lem1 x = case x of Z -> QED
[13:25:01] Dimitrios Vytiniotis: S x -> using (lem1 x) (another_lemma x)
[13:25:41] Koen Claessen: we cannot show non-termination
[13:25:53] Koen Claessen: which means we cannot mask BAD with non-termination
[13:25:59] Koen Claessen: mask BAD with UNR
[13:26:30] Koen Claessen: UNR is the only non-termanation that we can show
[13:26:44] Koen Claessen: (have a definition f = f in Haskell, just becomes f = f as an axiom)
[13:26:50] Koen Claessen: f = UNR
[13:27:21] Koen Claessen: (let x = x in x) `seq` BAD
[13:27:24] Koen Claessen: does not crash
[13:27:37] Koen Claessen: BAD `using` non_terminating_lemma
[13:28:08] Dimitrios Vytiniotis: UNR `using` bad_returning_lemma
[13:30:05] Koen Claessen: {{ x | p x }} as ashortcut for { x | p x } && CF
[13:31:29] Dimitrios Vytiniotis: S BAD ?
[13:32:53] Koen Claessen: we added && and ||
[13:33:50] Koen Claessen: < x | p x >
[13:34:10] Koen Claessen: ( x | p x )
[13:34:28] Koen Claessen: { x | p x }
[13:46:20] Koen Claessen: SPASS
[13:46:56] Koen Claessen: paradox
[13:47:26] Koen Claessen: paradox finds finite models
[13:50:32] Koen Claessen: min meands iM INterested
[13:52:39] Dimitrios Vytiniotis: a_x
[13:52:48] Dimitrios Vytiniotis: a_X := ............
[13:54:51] Koen Claessen: X = Y
[13:54:56] Koen Claessen: X = a
[13:55:16] Koen Claessen: cnf(axiom, axiom, X = Y).
[13:55:25] Koen Claessen: fof(axiom,axiom, ![X,Y] : X=Y).
[13:57:54] Koen Claessen: Koen is on Xmas holiday 20/12 - 2/1
[13:58:23] Dimitrios Vytiniotis: DImitrios 24/1 - 3/1 inclusive
[13:58:44] Dimitrios Vytiniotis: cabal install cmdargs
[13:59:07] *** Call ended, duration 36:10 ***
Koen Claessen