Macros and FAQ

Hi,

I cleaned up and extended my macros for formulae, derivations and now 
also atomic flows. They're available at 
<http://alessio.guglielmi.name/res/vl/>. They supersede the previous 
macros (DedStraker and earlier) but they're not compatible, because 
the cleaning up entailed some changes in their usage. If you want to 
see something fixed or implemented, please let me know.

Prompted by a referee, I wrote the below FAQ entry (for the page 
<http://alessio.guglielmi.name/res/cos/faq.html>). Comments always 
welcome.

BTW, I've had for a long time the intention to transfer the deep 
inference pages to a wiki, so that everybody can edit them and they 
don't look as personal as they look now. Tom has a prototype already, 
but, so far, I couldn't find the time to do the transfer. Hopefully, 
we will do it before the end of the year. In the meantime, please let 
me know if there are additions or corrections you want me to do.

Ciao,

-Alessio


The good properties of the proofs in the calculus of structures are 
obtained by an extensive use of hidden equalities; are you cheating?

No, we are not cheating. The equations are exclusively used in 
correspondence of invertible, linear inference rules. These inference 
rules do not alter the geometry of proofs, in the sense of relation 
webs, proof nets and atomic flows, for example. So, it is convenient 
to work on formulae modulo these equations, because we get much 
closer to the semantics of proofs. This comes at the expense of an 
immediate understanding of the calculus of structures in terms of 
proof search. However, fully syntactic systems can be obtained by 
simply turning equations into inference rules, and this only blows 
polynomially the size of proofs, without destroying any good 
property, like locality and normalisability, for example.