A contribution to automated-oriented reasoning about permutability of sequent calculi rules | Zendy

Tatjana Lutovac | Zendy; James Harland | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A contribution to automated-oriented reasoning about permutability of sequent calculi rules

Author(s) -

Tatjana Lutovac,

James Harland

Publication year - 2013

Publication title -

computer science and information systems

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.244

H-Index - 24

eISSN - 2406-1018

pISSN - 1820-0214

DOI - 10.2298/csis120820043l

Subject(s) - sequent , sequent calculus , completeness (order theory) , cut elimination theorem , computer science , permutation (music) , calculus (dental) , natural deduction , representation (politics) , mathematics , algorithm , proof calculus , discrete mathematics , mathematical proof , law , medicine , mathematical analysis , physics , geometry , dentistry , politics , political science , acoustics

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research