Hi, Sorry about this message. It seems that this person might be spamming. I've taken the action

Hi , Greetings from PERI Software Solutions. This is Shrudhi, Would like to talk to you regarding

Posting email from Warren. Hi Dustin, No, we are not having class tomorrow (Thursday). Noone

I am slightly confused; are we or are we not having class this Thursday and the following Tuesday?

Hi, If I were trying to use induction directly, here's probably the induction I would use: x <

Hi, Here's a message from Warren, clarifying the confusion some of you had regarding the

Hi, I'm attaching the ACL2 log of today's demo by Matt Kaufmann. Matt has also put the log on

This post is just to clarify that we've submitted our formal request to Sandip.

[ Sorry, resending since I forgot to CC Matt in the last email. ] Hi, Matt Kaufmann (CCed) has

OK, we have an initial offer of having Sandip do #50, #51 and #55. My guess is that #51 is the most

Hi, I want to keep myself out of the problem selection, but I want to add something. Please make sure

Sure, I can show you. But as far as I can see ACL2 proves the theorem automatically (with my

Hi, I got some queries regarding the level of detail necessary in answering the proof exercises, and

Hi, I don't understand what you mean by "we were not supposed to assume our hypothesis true

This was a good email reply from Sandip to a general question I had about this class that I thought

Hi, [ I am copying Matt Kaufmann and J Moore, in case they have further clarifying remarks to make in

Hi, I thought I'd post a solution to the OR-implication exercise that I suggested in class a week

In the class last Thursday, we saw a proof of the Deduction Law. Some of you seem to have been

Hi Jeff, You're right. Since the logic is applicative there is no destructive updates (at least

Hi, I class I gave the following derived rule of inference (without proof), and left the proof as an

Hello Students, Since this mailing list was created with the idea of students using Gmail accounts to

Hi, I thought I'd add a few things. In a certain sense you cannot write '(1 2 *PI*) as a term

As mentioned in another email, I was having false negatives due to a character translation error when

I solved the quoting issue. It's not true that redundant quotes are illegal - they do in fact

Much thanks to Sandip and Matt for all the time they spent helping me get ACL2 installed on my Mac. I