scientific article; zbMATH DE number 1301758

MaRDI QIDQ4246973zbMATHFDO

Authors Rajeev Goré, Jeremy E. Dawson

Publication date 12 January 2000

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)

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

Cited in

(8)

• On Automating the Calculus of Relations
• Proper multi-type display calculi for rough algebras
• scientific article; zbMATH DE number 1614695 (Why is no real title available?)
• Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle
• scientific article; zbMATH DE number 1927419 (Why is no real title available?)
• RALL: machine-supported proofs for relation algebra
• A new machine-checked proof of strong normalisation for display logic
• scientific article; zbMATH DE number 1735911 (Why is no real title available?)

Describes a project that uses

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)