Proceedings First International Workshop on Focusing

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 languages and rewriting calculi.