A Contribution to Automated-oriented Reasoning about Permutability of Sequent Calculi Rules

Tatjana Lutovac1 and James Harland2

  1. Department of Applied Mathematics, Faculty of Electrical Engineering,
    University of Belgrade, P.O. Box 35-54, 11120 Belgrade, Serbia
  2. School of Computer Science and Information Technology, RMIT University
    GPO Box 2476V, Melbourne, 3001, Australia


Many important results in proof theory for sequent calculus (cut-elimination, completeness and other properties of search strategies, etc) are proved using permutations of sequent rules. The focus of this paper is on the development of systematic and automated-oriented techniques for the analysis of permutability in some sequent calculi. A representation of sequent calculi rules is discussed, which involves greater precision than previous approaches, and allows for correspondingly more precise and more general treatment of permutations. We define necessary and sufficient conditions for the permutation of sequence rules. These conditions are specified as constraints between the multisets that constitute different parts of the sequent rules. The authors extend their previous work in this direction to include some special cases of permutations.

Key words

Automated reasoning, permutation, sequent calculi, proof search, linear logic

Digital Object Identifier (DOI)


Publication information

Volume 10, Issue 3 (June 2013)
Year of Publication: 2013
ISSN: 1820-0214 (Print) 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

Lutovac, T., Harland, J.: A Contribution to Automated-oriented Reasoning about Permutability of Sequent Calculi Rules. Computer Science and Information Systems, Vol. 10, No. 3, 1185-1210. (2013)