Proceedings Seventh International Workshop on Classical Logic and Computation

TL;DR

This special issue summarizes the seventh CL&C conference, focusing on the computational aspects of various logics, including normalization, cyclic proofs, and complexity, with empirical and theoretical contributions.

Contribution

It presents new reduction sets for intuitionistic logic extensions, an empirical comparison of normalization algorithms, and a polynomial-time checking method for cyclic proofs.

Findings

Empirical comparison of normalization algorithms' time consumption

New reduction sets for intuitionistic logic extensions with Herbrand disjunction property

Polynomial-time algorithm for checking correctness of certain cyclic proofs

Abstract

This special issue cover the seventh and last conference of the CL&C series, started in 2006 in San Servolo. Topics are the computational content of logics between intuitionistic logic and classical logic, through normalization, and a new topic, cyclic proofs and the complexity of checking the correctness of a cyclic proof. Accepted papers include an empirical comparison of time consumption of different normalization algorithms, and new reductions sets for several extensions of intuitionistic logic having the Herbrand disjunction property. Another paper provides a reduction set for admissible rules for intuitionistic logic. A paper describes a subset of cyclic proofs having a polynomial-time algorithm checking correctness.