Proceedings First International Workshop on Focusing
Iliano Cervesato (Carnegie Mellon University), Carsten Sch\"urmann (IT, University of Copenhagen)

TL;DR
This paper presents proceedings from the first international workshop on focusing, highlighting its significance as a proof search strategy that enhances logic programming and reasoning.
Contribution
It introduces the concept of focusing, discusses its applications in computational logic, and showcases recent developments and research presented at the workshop.
Findings
Focusing is a complete proof search strategy for many logics.
It alternates between inversion and chaining phases for efficient proof search.
The workshop included four selected papers and an invited talk on focusing.
Abstract
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. 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
