Uniformize Entry Titles

[ceilican]

The following entries are affected:

TODO

[vcvpaiva]

don't quite follow. what do you mean?

[ceilican]

Right now entry titles follow one of the naming schemes below:

1) just the name of the calculus without specifying the logic (e.g. "Superposition", "Resolution", ...).

2) name of the calculus plus logic for which the calculus was designed (e.g. "Classical Sequent Calculus LK", "Intuitionistic Sequent Calculus LJ", ...).

3) Just the name of the logic (e.g. "Intuitionistic Linear Logic", "Full Intuitionistic Linear Logic", ...).

4) Name of the calculus plus name of a theorem prover implementing the calculus (e.g. "Bledsoe's Natural Deduction - Prover", "Natural Knowledge Bases - Muscadet").

Firstly, we should strive to have a standard naming scheme, for the sake of uniformity and style.

Among the 4 naming schemes above, I prefer the second. The problem with the second is that titles can become too long. A solution has to be found for such cases.

I find the first naming scheme acceptable, if it is clear for which logic the calculus has been designed.

The third naming scheme is not informative enough. It also gives the impression of conflating the notions of logic and calculus. I think some people would advocate in favor of such a conflation, but this is not a mainstream opinion. Although I don't want to dive into a philosophical discussion of what is a logic and what is a calculus at this point, I think it would be useful to informally distinguish these two notions and make it clear that the Encyclopedia is, at this point in time, primarily about calculi, not about logics. (In the future, it would be nice to have introductory chapters about logics as well... But that is another story...)

The fourth naming scheme is too informative. Information about implementations is very interesting, but I think it should be handled in a different way, not in the titles.

Suggestions are welcome!

( @vcvpaiva : is it clearer now? )

[vcvpaiva]

yes, clearer now, thanks.

but of course the problem is that LK stands for classical logic sequent calculus, because of consolidated tradition, it's from 1930 and apart from the use (or not) of Gothic letters, there is no discussion. Of course people might prefer classical logic in Kleene's style sequents or Schutte's style sequents, though.as well as in axioms or Natural Deduction. (as far as I remember these are not in the Encyclopedia, right?)

Now, if I say "K" you might presume I am talking about a set of axioms for basic modal logic, but this is not uncontroversial. there is even more variation. so it's easy to transform "Intuitionistic Linear Logic" to "Sequent Calculus for ILL" and hopefully everyone would know that I am talking about the system in Lafont and Girard 1987, but not absolutely clear.

Since people contribute what they're fond of uniformization might be complicated. But worth trying for, I am sure.

[ceilican]

Thanks for the remarks, @vcvpaiva !

[vcvpaiva]

Even if we don't uniformize completely titles, I wish we could make the existing titles more informative. I believe even the most traditional ones could be renamed as Gentzen sequent calculus LJ, Kleene's G3, etc..

[ceilican]

That's a good idea. The challenge (in some cases) is to make all the information we would like to have in the title fit in one line.