Bleg: Systematic Approaches to Generation of Logical Calculi

Over lunch the other day, my friend and colleague Agata Ciabattoni told me about her paper at this year’s LICS, “From axioms to analytic rules in nonclassical logics“. In it, she and her co-authors Nikolaos Galatos and Kazushige Terui present an intriguing and very general result: Suppose you have a logic which can be axiomatized in full Lambek calculus with exchange (that’s intuitionistic logic without weakening or contraction, but with exchange) by adding axioms. If the additional axioms aren’t too complex, there’s a systematic way of generating an analytic hypersequent calculus for your logic, i.e., a systematic way of converting the additional axioms into a structural rule for a hypersequent calculus in such a way that cut is eliminable. This procedure applies to a wide range of substructural logics but also superintuitionistic logics. (UPDATE: more detail in the next post.) So that got us thinking: what other general, systematic approaches to generation of calculi are there? Agata’s approach generates calculi of a specific form (hypersequent calculi) from other calculi (Hilbert-style calculi). Then I know of two approaches that systematically generate calculi from a semantics. Arnon Avron, Beata Konikowska, and Anna Zamansky have been doing a lot of work on logics given by what they call non-deterministic matrices. I wrote a while ago about the approach I detailed in my undergraduate thesis, which goes back to work by Rousseau in the 1960s: systematic (i.e., automatic) generation of sequent, tableaux, natural deduction calculi for a logic given by finite truth tables. These are the only systematic results I know of, but that just shows my ignorance! There must be others! I’m sure there are general results in modal correspondence theory, for instance, to obtain axioms and perhaps tableaux systems, etc., for modal logics from conditions on frames. Can anyone help me (and Agata) out here?

2 thoughts on “Bleg: Systematic Approaches to Generation of Logical Calculi

  1. Richard, on this issue I would like to recommend you and Agata to have a look at our paper Two’s company: “The humbug of many logical values”, a preprint of which can be found here. We exhibit there a constructive procedure for reducing a ‘sufficiently expressive’ finite-valued into an alternative adequate (non-truth-functional) bivalued semantics, and show next how to extract 2-signed tableau systems from that. Other important papers on the issue are mentioned at the bibliography of that paper, in particular the paper by Carnielli at the JSL in 1987, where he extends the work of Rousseau that you mentioned.For an even more practical work on the automatic generation of classic-like (non-analytic) tableaux for finite-valued logics, I have delivered this year a paper at IJCAR in Sydney, where we implement the algorithm mentioned in the above paper in order to generate theory files ready to use by the Isabelle proof assistant. The corresponding paper, currently submitted for publication, is called Towards fully automated axiom extraction for finite-valued logics, and I will send a copy directly to your email and to anyone else who manifests interest on it. You might also like to have a look at this implementation in ML.Finally, on the extraction of axioms for modal systems, there is some nice work done by Renate Schmidt, please do have a look at her webpage.

Leave a Reply

Your email address will not be published. Required fields are marked *