Labelled Tableux
Yes, I know that Greg scooped me on this one, but Thomas Sutton has started a blog charting his development of a modal logic theorem prover written in Haskell and based around labelled tableaux. I point you to: Labelled Tableaux.
Labelled what you ask? A tableau is a proof theoretic gadget that looks and feels much like a collection of "uspide down sequent rules". The idea of tableaux is that instead of proving a formula, we show that its negation is inconsistent with the logic. This works especially well in the case of modal logic, since the tableau rules tend to match the frame semantics quite closely. Moreover, if the statement is not a theorem, then we can extract a countermodel from the failed proof search. This is quite dandy! For an introduction to tableau calculi for modal logic, including as much modal logic as is required, see:
Tableau Methods for Modal and Temporal Logic, Rajeev Gore'
(Full disclosure: Raj is one of my PhD supervisors. Of course, I give the article three thumbs up :)
So, what is all this labelling about then? Well, modal proof theory is a tricky thing to get right. In order to avoid nasty things such as infinite looping during proof search, many people have incorporated "labels" into their tableau calculi. This is not so nice from a theoretical point of view, since it obfuscates the essence of the logic and has a very "hacky" feel to it. Of course, if you are actually building a theorem prover, then labels are very handy!
A question that occurs to me is whether anyone has beaten semantic tableaux into providing systems for paraconsistent logics. This is a family of logics where an inconsitency does not necessarily trivialise the theory. Or, alternatively, where both a statement and its negation can be theorems! The basic strategy of attacking the negation of a formula seems, at first glance, to be at odds with this property. I'd be interested in any work that proves me otherwise.
Anyway, I'll be interested to see how the project turns out for Thomas. Maybe he'll let me play around with it when he is done... :)
posted by Jon @ 10:34 PM
10 Comments:
Jon --
I presume Labelled Tableaux are (or can be) related to Labelled Deductive Systems, an idea with immense and mostly as-yet-unrealized potential. An LDS is a logical system together with a collection of labels for wffs, with rules of inference for the wffs and associated rules for combination of the labels. Dov Gabbay wrote the first book on the subject "Labelled Deductive Systems". The AI Lab at Cancer Research UK has applied these ideas to design of medical expert systems.
Posted by Peter McB.
Technically, aren't most paraconsistent logics just weakenings of classical logic, so that no statement and its negation are both theorems? If both are premises, then in general not everything is a conclusion, but that's not quite the same. But I think it's still the case that everything that's not a theorem has a countermodel, and I think no theorems have countermodels (since they're all classical theorems as well). Unless you're building the premises into the proof system somehow.
Posted by Kenny Easwaran
Peter: I have heard of Gabbay's book but, alas, my library does not have a copy, so I haven't actually seen it...
Kenny: I think it all depends on what you call paraconsistent logic. I think what you are suggesting encompasses what I would call substructural logics. Terminology varies though. A lot of people call them linear logics, still others call them relevant logics (extending the term beyond only systems of relevant implication). There most likely are models of paraconsistent logic where all nontheorems have a countermodels...I suspect that such models would be based on ternary relations (a wild guess, I really don't know the area very well at all)...
Posted by Jon
"A question that occurs to me is whether anyone has beaten semantic tableaux into providing systems for paraconsistent logics."
I haven't seen a copy myself, but I seem to recall Koji telling me once that he did a bit of this in his thesis. [Koji Tanaka. A labyrinth of trees and the sound of silence : topics in dialetheism. PhD thesis. UQ. 2000.]
Posted by Nick Smith
Nick: Thanks for the pointer! If nothing else, that is a fantastic thesis title :) I wonder if his use of the word "labyrinth" is a tip towards Borges?
Posted by Jon
You can also modify the tableau method so that to prove the validity of A, you start the tree with A rather than its negation, which is more direct. H. Leblanc has an article about it in the Notre Dame Journal of Formal Logic.
By 'labelling' if you mean prefixing two labels T,F for truth and falsehood to formulas, then one benefit is that it sometimes yields more compact proofs and rules (than simply using negation). But I don't think that's what you mean wrt to automated reasoning. Does that linked-to article explain more?
Posted by lumpy pea coat
lpc: Thanks for the reference! My initial thoughts are that the "dual smullyan trees" are not really all that different. That is, instead of dualising at the root (that is, starting with ~A), one dualises at the level of rules and looks for things to close (allowing one to start from A).
Raj's article does indeed explain labels in more detail -- check out the stuff starting from the bottom of page 79. Labels are used in a different manner to the way you suggest. The idea of the labels in these systems is to keep track of your travels through the Kripke model in an explicit manner.
Posted by Jon
No, they aren't much different, but Duals of Smullyan trees closely resemble (upside down) Gentzen trees since the occurrence of the origin is shown to be irrefutable (rather than the negation shown to be unsatisfiable).
Just reading Raj's article now--a lot is either taken from or similar to Fitting. (Fitting uses "prefixed" vs. "labelled".) What I like about Raj's article is that it works with provability logics (e.g. G). I'll have to read more later. Thanks for linking.
Posted by lumpy pea coat
i buy hydrocodone at buy hydrocodone - can't find any cheaper
Dear all:
This is going to be probably the latest comment left on a blog ever (I am reacting four years later to a comment left in 2005)... but in any case, in 2005 somebody asked:
"A question that occurs to me is whether anyone has beaten semantic tableaux into providing systems for paraconsistent logics. This is a family of logics where an inconsitency does not necessarily trivialise the theory. Or, alternatively, where both a statement and its negation can be theorems! The basic strategy of attacking the negation of a formula seems, at first glance, to be at odds with this property. I'd be interested in any work that proves me otherwise."
I just want to tell that since 18 years ago tableaux have been produced for paraconsistent logics; I list the main work of our group in Brazil, but other people have contributed as well:
[1]- W. A. Carnielli, L. Fariñas del Cerro, and M. Lima-
Marques. Contextual negations and reasoning with
contradictions. In Proc. of the 12th Int. Joint Conf.
on Artificial Intelligence IJCAI-91.
[21]- W. A. Carnielli and M. Lima-Marques. Reasoning
under inconsistent knowledge. J. of Applied Non-
Classical Logics, 1992
[3]- W. A. Carnielli and J. Marcos. Tableaux for logics of formal inconsistency. In H. R. Arabnia, editor, Proceedings of the International Conference on Artificial Intelligence (IC-AI'2001), volume II, pages 848--852. CSREA Press, Athens GA, USA, 2001.
available from:
http://docs.google.com/gview?a=v&q=cache%3Aw860yUlyVyEJ%3Asqig.math.ist.utl.pt%2Fpub%2FMarcosJ%2F01-CM-tableaux.pdf+tableaux+%22paraconsistent+logics%22&hl=pt-BR&gl=br&sig=AFQjCNEfsrzjnmkIj1em3w_jHarYlbtdzA&pli=1
[4]- W. A. Carnielli(with M. E. Coniglio and J. Marcos). Logics of Formal Inconsistency. In: Handbook of Philosophical Logic, vol. 14, pp.15-107. Eds.: D. Gabbay; F. Guenthner. Springer, 2007 (withc M. E. Coniglio and J. Marcos).
available from:
http://www.cle.unicamp.br/e-prints/vol_5,n_1,2005.html
Best regards,
Walter Carnielli
Post a Comment
<< Home