Mechanized Formalization of Proof System

[viveknigam]

• Users should be able to easily find mechanized formalization of proof systems (and their meta-theory). This can be achieved by adding links to the proof scripts/code or to the paper mentioning it.

• Observations can be inserted about (minor) differences between the paper proof system and the mechanized specification. For example, the use of LJ additive rules instead of multiplicative ones or vice versa.

• Finally, there may be several mechanized formalizations. One could also add a field detailing their differences.

[ceilican]

An index in the end of the encyclopaedia could be helpful as well or instead.

[ceilican]

See #71, which partially addresses this suggestion.

[olaure01]

Ongoing work on gathering formalizations of linear logic.