Geodesic
A Contribution to Automated-oriented Reasoning about Permutability of Sequent Calculi Rules
Computer Science and Information Systems, Tome 10 (2013) no. 3.

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

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.
Keywords: Automated reasoning, permutation, sequent calculi, proof search, linear logic 
@article{CSIS_2013_10_3_a12,
     author = {Tatjana Lutovac and James Harland},
     title = {A {Contribution} to {Automated-oriented} {Reasoning} about {Permutability} of {Sequent} {Calculi} {Rules}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {10},
     number = {3},
     year = {2013},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2013_10_3_a12/}
}
TY  - JOUR
AU  - Tatjana Lutovac
AU  - James Harland
TI  - A Contribution to Automated-oriented Reasoning about Permutability of Sequent Calculi Rules
JO  - Computer Science and Information Systems
PY  - 2013
VL  - 10
IS  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2013_10_3_a12/
ID  - CSIS_2013_10_3_a12
ER  - 
%0 Journal Article
%A Tatjana Lutovac
%A James Harland
%T A Contribution to Automated-oriented Reasoning about Permutability of Sequent Calculi Rules
%J Computer Science and Information Systems
%D 2013
%V 10
%N 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2013_10_3_a12/
%F CSIS_2013_10_3_a12
Tatjana Lutovac; James Harland. A Contribution to Automated-oriented Reasoning about Permutability of Sequent Calculi Rules. Computer Science and Information Systems, Tome 10 (2013) no. 3. http://geodesic.mathdoc.fr/item/CSIS_2013_10_3_a12/