scientific article; zbMATH DE number 1301758

zbMATH Open0928.03007MaRDI QIDQ4246973FDOQ4246973

Authors: Rajeev Goré, Jeremy E. Dawson 

Publication date: 12 January 2000

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

Recommendations

• scientific article; zbMATH DE number 1927419
• scientific article; zbMATH DE number 1086668
• RALL: machine-supported proofs for relation algebra
• A new machine-checked proof of strong normalisation for display logic
• scientific article; zbMATH DE number 1735911

zbMATH Keywords

automated deductiondisplay logicdescription logicsrelation algebraproof searchproof systemsautomatic cut-elimination procedureinteractive proof assistantIsabelle theory

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)

• Proper multi-type display calculi for rough algebras
• Title not available (Why is that?)
• RALL: machine-supported proofs for relation algebra
• Title not available (Why is that?)
• On Automating the Calculus of Relations
• A new machine-checked proof of strong normalisation for display logic
• Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle
• Title not available (Why is that?)

Uses Software

• Isabelle
• RALL

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 Q4246973)