(1) Institute für Computersprachen TU Wien, Favoritenstrasse 9-11, Wien, 1040, Austria;(2) National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan
Abstract:
We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.