RALL: Machine-supported proofs for relation algebra

DOI10.1007/3-540-63104-6_36zbMath1430.68425OpenAlexW1503466517MaRDI QIDQ5234720

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

relation algebraIsabelleatom structureinteractive and automatic theorem proving

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)

Related Items (2)

Typing theorems of omega algebra ⋮ On Automating the Calculus of Relations

Uses Software

• Isabelle
• Isabelle/HOL
• Ralf
• RALL

Cites Work

• Term rewriting and beyond -- theorem proving in Isabelle
• On fuzzy difunctional relations
• An algebraic formalization of fuzzy relations
• Isabelle. A generic theorem prover
• The representation of relational algebras
• Relational Methods in Computer Science
• Boolean Algebras with Operators. Part I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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