APPA 2014 VSL PROCEEDINGS: EDITOR'S PREFACE

Many of us, logicians, work toward the improvement of proofs, proof systems, proof formats, interactive proof script languages, proof search methods, etc. But what makes a proof (system|format|search-method|etc.) better than another? Logicians from different communities will give radically different answers to this question! The principles behind their answers may be unknown to outsiders; they may even sound obscure, ungrounded or in apparent contradiction to the principles of other communities.

The debate about the importance of proofs and what makes some proofs better than others has a long tradition that is probably as old as logic itself. In the modern era we could, for example, quote Poincare's opinion that "a collection of facts is no more a science than a heap of stones is a house"; cite Hilbert's unpublished 24th problem; and mention Kreisel's proof unwinding program and his question of "what more do we know if we have proved a theorem by restricted means other than if we merely know the theorem is true?". With the current multitude of proof-generating deduction tools, proof systems and practical applications of proofs, this debate is more pertinent and lively than ever. But it seems unfortunately fragmented across many communities.

The Vienna Summer of Logic (VSL) presented a unique opportunity to promote a conversation between all the communities on questions related to proofs, and the goal of the APPA 2014 workshop (All about Proofs, Proofs for All) was to promote a fruitful knowledge exchange by organizing short tutorials given by prominent speakers from various communities. These tutorials were intended to be accessible to young researchers as well as to experienced researchers from other communities.

This volume contains the papers corresponding to the 12 invited talks presented at APPA 2014 held on July 18, 2014 in Vienna (Austria). In the preparation of these proceedings, Andrei Voronkov's EasyChair conference management system proved itself an excellent tool.