RALL: machine-supported proofs for relation algebra

DOI10.1007/3-540-63104-6_36MaRDI QIDQ5234720zbMATH OpenOpenAlexFDO

Authors David von Oheimb, Thomas F. Gritzner

Publication date 1 October 2019

Published in Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-63104-6_36

zbMATH Keywords

atom structureinteractive and automatic theorem provingIsabellerelation algebra

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cylindric and polyadic algebras; relation algebras (03G15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On Automating the Calculus of Relations
• scientific article; zbMATH DE number 1614695
• scientific article; zbMATH DE number 1301758
• scientific article; zbMATH DE number 762061
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL

Cites work

• An algebraic formalization of fuzzy relations
• Boolean Algebras with Operators. Part I
• scientific article; zbMATH DE number 3933071 (Why is no real title available?)
• scientific article; zbMATH DE number 3974258 (Why is no real title available?)
• scientific article; zbMATH DE number 193143 (Why is no real title available?)
• scientific article; zbMATH DE number 3537204 (Why is no real title available?)
• scientific article; zbMATH DE number 475192 (Why is no real title available?)
• scientific article; zbMATH DE number 709076 (Why is no real title available?)
• scientific article; zbMATH DE number 234018 (Why is no real title available?)
• scientific article; zbMATH DE number 3339390 (Why is no real title available?)
• scientific article; zbMATH DE number 3103212 (Why is no real title available?)
• Isabelle. A generic theorem prover
• On fuzzy difunctional relations
• Relational Methods in Computer Science
• Term rewriting and beyond -- theorem proving in Isabelle
• The representation of relational algebras

Cited in

(8)

• Typing theorems of omega algebra
• scientific article; zbMATH DE number 1614695 (Why is no real title available?)
• On Automating the Calculus of Relations
• scientific article; zbMATH DE number 1301758 (Why is no real title available?)
• scientific article; zbMATH DE number 1735911 (Why is no real title available?)
• scientific article; zbMATH DE number 762061 (Why is no real title available?)
• Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
• Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• Ralf
• RALL

This page was built for publication: RALL: machine-supported proofs for relation algebra

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