scientific article; zbMATH DE number 1927419

zbMATH Open1013.03011MaRDI QIDQ4484337FDOQ4484337

Authors: Rajeev Goré, Jeremy E. Dawson 

Publication date: 12 June 2003

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2410/24100131.htm

Title of this publication is not available (Why is that?)

Recommendations

• A new machine-checked proof of strong normalisation for display logic
• scientific article; zbMATH DE number 1301758
• Display calculi for logics with relative accessibility relations
• scientific article; zbMATH DE number 1086668
• Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35) Cylindric and polyadic algebras; relation algebras (03G15)

Cited In (8)

• Generic methods for formalising sequent calculi applied to provability logic
• Machine-checked meta-theory of dual-tableaux for intuitionistic logic
• Machine-checked interpolation theorems for substructural logics using display calculi
• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• Hypersequent and display calculi -- a unified perspective
• Craig interpolation in displayable logics
• Machine Checking Proof Theory: An Application of Logic to Logic
• Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4484337)