Using relation-algebraic means and tool support for investigating and computing bipartitions

DOI10.1016/J.JLAMP.2017.04.001MaRDI QIDQ2360655zbMATH OpenOpenAlexFDO

Authors Rudolf Berghammer, Insa Stucke, Michael Winter

Publication date 4 July 2017

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2017.04.001

zbMATH Keywords

bipartitionDedekind categorymechanised proofsrelation algebrarelational axiom of choicesplitting

Mathematics Subject Classification ID

Other classical set theory (including functions, relations, and set algebra) (03E20) Cylindric and polyadic algebras; relation algebras (03G15) Categories of spans/cospans, relations, or partial maps (18B10) Semantics in the theory of computing (68Q55) Symbolic computation and algebraic computation (68W30)

Recommendations

• Investigating and computing bipartitions with algebraic means
• An algebraic approach to binary relations.
• Binary relations. Addenda. 1: Kernel, restrictions and inducing, relational morphisms
• A relation-algebraic theory of bisimulations
• Relations: concrete, abstract, and applied. An introduction

Cites work

• An Ordered Category of Processes
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Automated verification of relational while-programs
• Complements in distributive allegories
• Computer Algebra in Scientific Computing
• Computing kernels in directed bichromatic graphs
• Deciding Kleene algebras in \texttt{Coq}
• Dedekind categories with cutoff operators
• Embedding mappings and splittings with applications
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 3683841 (Why is no real title available?)
• scientific article; zbMATH DE number 45228 (Why is no real title available?)
• scientific article; zbMATH DE number 193143 (Why is no real title available?)
• scientific article; zbMATH DE number 234018 (Why is no real title available?)
• scientific article; zbMATH DE number 2203240 (Why is no real title available?)
• scientific article; zbMATH DE number 3210031 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Investigating and computing bipartitions with algebraic means
• Isabelle/HOL. A proof assistant for higher-order logic
• Kleene algebra with tests and Coq tools for while programs
• Non-embeddable simple relation algebras
• On automated program construction and verification
• On Automating the Calculus of Relations
• Orders, lattices and relations with applications
• Relational and algebraic methods in computer science. 15th international conference, RAMiCS 2015, Braga, Portugal, September 28 -- October 1, 2015. Proceedings
• Relations among matrices over a semiring
• Tool-Based Verification of a Relational Vertex Coloring Program

Cited in

(2)

• Investigating and computing bipartitions with algebraic means
• Embedding mappings and splittings with applications

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• VAMPIRE

This page was built for publication: Using relation-algebraic means and tool support for investigating and computing bipartitions

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