Searching For A Closed Tableau
If a tableau calculus is complete, every unsatisfiable set of formula has an associated closed tableau. While this tableau can always be obtained by applying some of the rules of the calculus, the problem of which rules to apply for a given formula still remains. As a result, completeness does not automatically implies the existence of a feasible policy of application of rules that can always lead to building a closed tableau for every given unsatisfiable set of formulae. While a fair proof procedure is complete for ground tableau and tableau without unification, this is not the case for tableau with unification.
A general solution for this problem is that of searching the space of tableau until a closed one is found (if any exists, that is, the set is unsatisfiable). In this approach, one starts with an empty tableau and then recursively tries to apply every possible applicable rule. This procedure visits a (implicit) tree whose nodes are labeled with tableau, and such that the tableau in a node is obtained from the tableau in its parent by applying one of the valid rules.
Since one such branch can be infinite, this tree has to be visited breadth-first rather than depth-first. This requires a large amount of space, as the breadth of the tree can grow exponentially. A method that may visit some nodes more than once but works in polynomial space is to visit in a depth-first manner with iterative deepening: one first visits the tree up to a certain depth, then increases the depth and perform the visit again. This particular procedure uses the depth (which is also the number of tableau rules that have been applied) for deciding when to stop at each step. Various other parameters (such as the size of the tableau labeling a node) have been used instead.
Read more about this topic: Method Of Analytic Tableaux
Famous quotes containing the words searching for, searching and/or closed:
““Why were you searching for me? Did you not know that I must be in my Father’s house?””
—Bible: New Testament, Luke 2:49.
Jesus to his parents when they found him in the temple.
“A government deriving its energy from the will of the society, and operating, by the reason of its measures, on the understanding and interest of the society ... is the government for which philosophy has been searching and humanity been fighting from the most remote ages ... which it is the glory of America to have invented, and her unrivalled happiness to possess.”
—James Madison (1751–1836)
“Alas for the cripple Practice when it seeks to come up with the bird Theory, which flies before it. Try your design on the best school. The scholars are of all ages and temperaments and capacities. It is difficult to class them, some are too young, some are slow, some perverse. Each requires so much consideration, that the morning hope of the teacher, of a day of love and progress, is often closed at evening by despair.”
—Ralph Waldo Emerson (1803–1882)