We compare several methods of implementing the display (sequent) calculus RA for relation algebra in the logical frameworks Isabelle and Twelf. We aim for an implementation enabling us to formalise within the logical framework proof-theoretic results such as the cut-elimination theorem for RA and any associated increase in proof length. We discuss issues arising from this requirement.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-Free Deep Inference Calculi for S.Rajeev Gore - manuscript
Displaying the Modal Logic of Consistency.Heinrich Wansing - 1999 - Journal of Symbolic Logic 64 (4):1573-1590.
Display Calculi for Logics with Relative Accessibility Relations.Stéphane Demri & Rajeev Goré - 2000 - Journal of Logic, Language and Information 9 (2):213-236.
Encoding Modal Logics in Logical Frameworks.Arnon Avron, Furio Honsell, Marino Miculan & Cristian Paravano - 1998 - Studia Logica 60 (1):161-208.
Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.Rajeev Gore, Linda Postniece & Alwen Tiu - unknown
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads1 ( #872,365 of 2,158,464 )
Recent downloads (6 months)1 ( #354,692 of 2,158,464 )
How can I increase my downloads?