Talk:Method of analytic tableaux/Archive 1

Untitled

I know tableaux as semantic tableaux, and in fact, the page Semantic tableau redirects here. Is there a difference?

Not all tableau systems are analytic. This article could be generalized to include non-analytic systems. Nortexoid 20:48, 5 May 2006 (UTC)

Question

What program was used to make those diagrams? They look pretty nice. Is there a simple flow chart program out there that will whip those up? —Preceding unsigned comment added by 65.96.129.40 (talk) 21:41, 15 February 2008 (UTC)

Editing

This article isn't written very clearly. There is a lot of unnecessary terminology (e.g. 'multisets', 'sibling', 'child', etc.) that is left unexplained (e.g. 'branch', 'node', etc.). The article should be relatively brief and introductory. Am I the only one that finds it a disgusting mess?

Also, the title of the article should be something like 'Semantic tableau(x)' since there are tableau methods with cut rules. Nortexoid 01:26, 22 May 2006 (UTC)

Specific things to be cited

• "Clearly, we would prefer to always find the shortest closed tableaux but it can be shown that one single algorithm that finds the shortest closed tableaux for all input sets of formulae cannot exist." —Preceding unsigned comment added by Bayle Shanks (talk • contribs) 22:01, 20 November 2006

Possible Plagarism

This article looks like it might be ripe for plagarism accusation, I've read a few things on the page (for example "if σ is the most general unifier of two literals A and B, where A and the negation of B occurr in the same branch of the tableau, σ can be applied at the same time to all formulae of the tableau") that look like they have been copied verbatim from Melvin Fitting's book. His book is no doubt a good resource, and should be paraphrased (and perhaps his book elevated to the top of the list), but having chapter 6 and 7 from his book be a majority of the basis for the article is kind of sketchy.

Kmicinski 23:10, 5 January 2007 (UTC) Kristopher Micinski

Such an accusation would be groundless. No sentence has been directly lifted from Fittin's book, nor is any paragraph/section a direct sentence-by-sentence rephrasing from it. Referring to your example, what Fitting says is "Suppose T is a tableau [...], and some branch of T contains A and -B, where A and B are atomic. Then T\sigma is also a tableau ..." Not quite the same sentence I wrote. If you have other examples, please cite page and line numbers. Tizio 15:16, 7 January 2007 (UTC)

I'm not accusing you of anything, I've just noticed a simmilarity and thought that a few sentences might be possible plagarism. It's only a small portion of the article. Sorry about it, it just looked a lot like the material. I'll try to rework any more I see. I'll pull it from the copyright category. 207.210.205.28 23:00, 7 January 2007 (UTC)Kris Micinski

Thanks for clarifying. Of course, if you see that some sentences I wrote turned out to be too similar to some in Fitting's book (or some other sources), feel free to rephrase. Tizio 12:55, 8 January 2007 (UTC)

Terminology

The method is usually called (Semantic or Analytic) Tableaux (from French?) as the Title also indicates. In the body of the page though it is called Tableau. Should that be updated? DRap 09:09, 9 January 2007 (UTC)

Yes, the word originally entered English via French. "Tableaux" is plural (in both English and French, "Tableaus" is an alternative English plural, but rarely used, and, to my knowledge, never in this context), "Tableau" is singular. To add to the confusion, to my German ear, they both sound exactly the same ;-). --Stephan Schulz 09:20, 9 January 2007 (UTC)

Yes, perhaps we could clarify? You will often see in the article 'a tableau' and this should be made distinct from 'the tableaux' (is the 'x' silent?). I have seen it reffered to both as semantic tableaux and tableau, but don't which would be more appropriate here 207.210.205.28 04:32, 16 January 2007 (UTC) Kris Micinski

Contradiction

If a tableau calculus is complete, every unsatisfiable set of formula has an associated closed tableau that can be obtained by applying some of the rule of the calculus. However, this does not automatically implies that there is 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 with unification, this is not the case for tableau with unification.

Needless to say, the above paragraph is a contradiction. If an expert can please correct the article, that would be nice. -- Dragontamer (128.8.128.134 21:33, 25 October 2007 (UTC))

Ideas

Hi guys. Here are some thoughts. I wasn't very happy with the explanation of semantic tableaux given in Graham Priest's Introduction to Non-Classical Logic, I like this article even worse. Here's my interpretation of what I've understood so far:

• A semantic tableaux is a tree where each node contains a proposition.
• Put a proposition at the root node of the tree. You are about to test the truth of this proposition.
• Each node of the tree branches into the minimum number of nodes for at least one of the nodes to hold, given that its parent node holds.
• Whenever you find an obvious contradiction on a branch (ie, the branch requires A and not-A to simultaneously hold) close the branch.
• Keep applying this procedure until you've closed all the branches, or you're down to atomic propositions. If all the branches close, the root proposition is false, if none of them do then it's a tautology, if some of them are closed and some open then it's conditionally true. - Conskeptical 12:03, 26 October 2007 (UTC)

Empty model and Unification

The formula $\forall x.\gamma (x)\land \neg \gamma (x)$ is clearly satisfyable by the empty model. How is guaranteed that the First-order tableau calculus with unification will not lead to a contradiction? --94.217.196.40 (talk) 15:38, 3 October 2014 (UTC)

What you wrote has a predicate in it. Maybe there's another rule that says predicates cannot be canceled, unless the domain of discourse is checked first (to rule out the empty model). But the rest of this article doesn't talk about models, anyway, so ... ? 67.198.37.16 (talk) 03:40, 29 November 2023 (UTC)

Formatting of set-labeled tableau example

I do not know if this is a general problem but at least in my windows desktop computer using firefox the set-labeled tableau example is rendered incorrectly. It gets new lines in places that turn it into non-sense. I had to copy and paste it into a notepad to see what it is being formulated. ArelEu (talk) 12:42, 27 February 2023 (UTC)

I converted to latex just now. It's readable. And its actually kind of nice, much easier to understand than some of the earlier mumbo jumbo in this article. Turns out it's just perfectly direct and ordinary proof-theory reduction. I'm not sure why the rest of this article makes such a big deal about closure; it looks like something you'd find in any book on proof theory. What can I say, I guess I've got ADHD. 67.198.37.16 (talk) 03:32, 29 November 2023 (UTC)