[mathprog] Trees algorithm - finally finished
- From: Noam Petrank <buga@xxxxxxxxxxxxx>
- To: mathprog@xxxxxxxxxxxxx
- Date: Sat, 21 Sep 2002 17:29:58 +0300 (IDT)
After a week-late I'm glad to announce we have an algorithm!
It is attached in the files "SentenceTree.cpp", SentenceTree.h
For those of you who don't know the algorithm, I'll give a short
introduction of what it does.
When I find the time, I would also give an explanation of its
implementation and efficiency in our program, and share some thoughts
(Yonatan's and mine) of future improvement of this alg.
1. Introduction:
The truth trees system is a naive algorithm, which gets a set of sentences
in first-order logic (it doesn't handle in higher orders), plugging and
discharge them, building a binary tree of sentences. Each branch in the
tree is a different possible "world" (meaning) of the sentences.
It has about 15 rules of how to discharge a sentence.
if a branch has a contradiction, meaning, sentences in the forms "F" " not
F", or not(A=A), where A is a constant, it is considered closed.
if it is impossible to discharge sentences in a branch, it is considered
full. if a tree (finite or infinte) has a full open branch, then it is
open, and the sentences in its root are consistent.
Maybe Yonatan will send a copy of his book which specify them exactly.
Notes:
1. I've yet to debug the "forall" and "exists" parts of the alg'. If you
find any bugs inform me and I'll fix them.
2. The program was first written in xemacs, than in edit+, and compiled in
xemacs. Therefore, The Indention is ugly. If anyone volunteers, fix it.
3. When I started to write the alg' I thought that the queues should not
be members of the class. As long as the program grew, there were added
lots of methods which use the queues.
So, now it has some methods with 8 paramenters.
I'll change that, and send an update to the list. The methods are
createLeaves, insertToLeaves, insertToQueue, and discharge Methods.
4. There are some long methods (80 lines), but after a talk with Yonatan,
we have decided to keep them, since they are built in the form of "else
ifs".
5. right now, the alg does not support functions, but this can be easily
fixed by changing the substitutions methods.
Noam (buga).
Other related posts:
- » [mathprog] Trees algorithm - finally finished
