[mathprog] Re: Code!
- From: Yonatan Ben-Yaakov <yontanbn@xxxxxxxxxxxxx>
- To: mathprog@xxxxxxxxxxxxx
- Date: Sun, 8 Sep 2002 12:33:20 +0300 (IDT)
Well, I tried for it to be well-written, but it's actually even less than
a naive algorithm for the proof-machine. It's only the data-structure for
it.
I think it's good for us to start with a naive algorithm and then try to
improve it. Mabye at some point it will be dumped in favor of something
completely different, but I want to see my program proving things in the
following 1-2 weeks. Otherwise, I will probably lose hope. The reason this
project didn't succeed so far is that we sat and had meetings, and tried
to read books, etc... instead of programming. Now we're programming. When
we're done with this part (or it can be done in parallel) we'll think
about how to continue.
Now, a definition of this part (again, not yet finished, i want it to be
finished within 1-2 weeks.
Attempt to prove first-order logic statements, by proving a contradiction
in the set of assumptions (plus axioms [also in first order logic]), with
the added sentence which is the negation of the conclusion. This is done
by using a method called the "Tree method", taught in the course "mavo
letorat hahigayon" (given for philosophers.. ouch..), using brute-force
upon nondeterminism, and bounding the number of levels by a constant.
When you say "find the mailing list" what do you mean?
When you sent mail to mathprog@xxxxxxxxxxxxx it gets sent to everyone in
the list...
you want to know who the people on it are? i can tell you :)
Ruth Lawrence wrote open U books?! cool :)
But a tad irrelevant to this mailing list...
- Yonatan.
On Sat, 7 Sep 2002, Amit Levine wrote:
| didn't have the time to read it, but a quick look showed me that you sat
| down and programmed a naive algorithm for the "proof-machine". was it
| realy necessery? (if so- how) do you think a good solution will be based
| upon this algortihm? it seems tobe well-written. but I realy barely
| looked. I'll read it when I have the time and send you my opinion
|
| anyway- I guess a journey of a thousand miles begins with one step
|
|
| BTW- where can I find the mailing list?
|
| P.S
| (your calculus professor wrote the openu's infi 3 course)
|
| Amit W.
| Levine (how formal is that?)
| Yonatan Ben-Yaakov wrote:
|
| >Hey all
| >We finally have some code...
| >Attached is today's version
| >
| >- Yonatan.
| >
| > atp_8_9_2002.tar
| >
| > Content-Type:
| >
| > APPLICATION/x-tar
| > Content-Encoding:
| >
| > BASE64
| >
| >
|
|
Other related posts:
