utexas-cs313k-spring2009

ACL2 FOREVER! On Sat, May 23, 2009 at 1:52 PM, David Rager <rag...@gmail.com> wrote: > Is

The final exam grade is still not there. Can you guys give us an estimated date when it will be up?

I'll third that. 2009/5/17 Sungjin <k_o_r_...@naver.com> Me 2 On 5월15일, 오후6시47분, Anar

ah yes, you got me there! On May 15, 1:12 pm, Behnam Robatmili <be...@cs.utexas.edu> wrote:

On Fri, May 15, 2009 at 9:56 AM, rizing_starz4 <rizing...@yahoo.com> wrote: > > Oh

Sure. On May 15, 1:20 am, "samnos...@gmail.com" <samnos...@gmail.com> wrote: > Can

Hi Everyone, It looks to me like ya'lls final is in WEL 1.308. We're pretty much guaranteed

I think so. My only nitpick is that you probably also want to quantify over "user" as well.

Hi all, Here are the answers to the practice test. Please notice: 1) There might be typos or errors

Yes, but also vice versa meaning that every relative is happy when x is happy. In other words, I

Yes. On Tue, May 12, 2009 at 1:18 PM, David S. <dsny...@gmail.com> wrote: > > #9 > 4

Hi all, I'm making a small change to problem 1 of the practice test: Behnam 1) Prove the

Hello everyone, I'll be holding extended office hours on Thursday from 3:00pm to 5:00pm in PAI

I have to cancel my office hours tomorrow, and since you'll be taking your exam during my normal

Hi everyone, It's to remind you that I'm holding my normal office hours today (Monday, May 11

Indeed, the correct question would concern, in ACL2 notation: ( (1 . 2) ) x ( (3 . 4) ) And the

Ian W. wrote: > Sure. The answer is... ooh, noo, wait, my internet is dying! I'll go > fix

With set builder notation {x : phi}, the formula phi may have quantifiers. For example, {x : exists y

This was a good question. Hope to see something like this on the test.

I don't know what you mean by "A {A1}". If you mean, let A = {A1} and B = {B1}, then

List all the elements of the set; wrap the list in curly braces. On May 2, 2:44 pm, todd <

Here's a rubric if ya'll want. Remember that you still need to specify counterexamples

OK, fair enough. You got me on this one. On Apr 29, 9:45 pm, Luke Gary <lukeg...@gmail.com>

You might need a theorem like 341 in your proof... On Apr 27, 9:15 pm, Aaron <R.aaron.jo...@gmail.

Ok. I see your point. {v : (v in A) & (v in ({v : (v in B) & (v in C)})} is a set and you

Hi everyone, Due to some emergencies, I need to change my office hour tomorrow (Monday, Apr 27) from

Compute the value of the four expressions with j = 0 and see how many different values you get... On

Here you go: (forall v : t) <--> { Taut: short circuit } (implies t (forall v : t)) <-->

I believe it should read: Write down the set of ys at which f is an identity for x. Ian On Apr 23, 2:

You can use forall-concl at that point (possibly doing an alpha conversion first, depending on your