A mechanised proof system for relation algebra using display logic

DOI10.1007/3-540-49545-2_18MaRDI QIDQ4246973zbMATH OpenFDO

Authors Rajeev Goré, Jeremy E. Dawson

Publication date 12 January 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-49545-2_18

zbMATH Keywords

automated deductionautomatic cut-elimination proceduredescription logicsdisplay logicinteractive proof assistantIsabelle theoryproof searchproof systemsrelation algebra

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1927419
• Cut-free display calculi for relation algebras
• 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

(10)

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

Describes a project that uses

Uses Software

• Isabelle
• RALL

This page was built for publication: A mechanised proof system for relation algebra using display logic

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