Published: 8th November 2015|
|Preface Iliano Cervesato and Carsten Schürmann|
|Towards the Automated Generation of Focused Proof Systems Vivek Nigam, Giselle Reis and Leonardo Lima||1|
|Proof Outlines as Proof Certificates: A System Description Roberto Blanco and Dale Miller||7|
|Realisability semantics of abstract focussing, formalised Stéphane Graham-Lengrand||15|
|Multiplicative-Additive Focusing for Parsing as Deduction Glyn Morrill and Oriol Valentín||29|
This volume constitutes the proceedings of WoF'15, the First International Workshop on Focusing, held on November 23rd, 2015 in Suva, Fiji. The workshop was a half-day satellite event of LPAR-20, the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning.
The program committee selected four papers for presentation at WoF'15, and inclusion in this volume. In addition, the program included an invited talk by Elaine Pimentel (UFRN, Brazil).
Focusing is a proof search strategy that alternates two phases: an inversion phase where invertible sequent rules are applied exhaustively and a chaining phase where it selects a formula and decomposes it maximally using non-invertible rules. Focusing is one of the most exciting recent developments in computational logic: it is complete for many logics of interest and provides a foundation for their use as programming languages and rewriting calculi.
This workshop had the purposes of bringing together researchers who work on or with focusing, to foster discussion and to report on recent advances. Topics of interest included: focusing in forward, backward and hybrid logic programming languages, focusing in theorem proving, focusing for substructural logics, focusing for epistemic logics, focused term calculi, implementation techniques, parallelism and concurrency, focusing in security, and pearls of focusing.
Many people helped make WoF'15 a success. We wish to thank the organizers of LPAR-20 for their support. We are indebted to the program committee members and the external referee for their careful and efficient work in the reviewing process. Finally we are grateful to the authors, the invited speaker and the attendees who made this workshop an enjoyable and fruitful event.
Iliano Cervesato and Carsten Schürmann