|Abstract||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||No categories specified (fix it)|
|Through your library||Only published papers are available at libraries|
Similar books and articles
Rajeev Gore, Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-Free Deep Inference Calculi for S.
Heinrich Wansing (1999). Displaying the Modal Logic of Consistency. Journal of Symbolic Logic 64 (4):1573-1590.
Stéphane Demri & Rajeev Goré (2000). Display Calculi for Logics with Relative Accessibility Relations. Journal of Logic, Language and Information 9 (2):213-236.
Arnon Avron, Furio Honsell, Marino Miculan & Cristian Paravano (1998). Encoding Modal Logics in Logical Frameworks. Studia Logica 60 (1):161-208.
Francesca Poggiolesi (2010). Display Calculi and Other Modal Calculi: A Comparison. Synthese 173 (3).
Rajeev Gore, Linda Postniece & Alwen Tiu, Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Recent downloads (6 months)0
How can I increase my downloads?