scientific article; zbMATH DE number 1927419

MaRDI QIDQ4484337zbMATH OpenFDO

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

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)

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

Cited in

(8)

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

Describes a project that uses

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)