TY - JOUR
T1 - Cardinality of relations and relational approximation algorithms
AU - Berghammer, Rudolf
AU - Höfner, Peter
AU - Stucke, Insa
N1 - Publisher Copyright:
© 2015 Elsevier Inc.
PY - 2016/2/1
Y1 - 2016/2/1
N2 - First, we discuss three specific classes of relations, which allow to model the essential constituents of graphs, such as vertices and (directed or undirected) edges. Based on Kawahara's characterisation of the cardinality of relations we then derive fundamental properties on their cardinalities. As main applications of these results, we formally verify four relational programs, which implement approximation algorithms by using the assertion-based method and relation-algebraic calculations.
AB - First, we discuss three specific classes of relations, which allow to model the essential constituents of graphs, such as vertices and (directed or undirected) edges. Based on Kawahara's characterisation of the cardinality of relations we then derive fundamental properties on their cardinalities. As main applications of these results, we formally verify four relational programs, which implement approximation algorithms by using the assertion-based method and relation-algebraic calculations.
KW - Approximation algorithm
KW - Assertion-based program verification
KW - Cardinality operation
KW - Relation algebra
UR - http://www.scopus.com/inward/record.url?scp=84995948216&partnerID=8YFLogxK
U2 - 10.1016/j.jlamp.2015.12.001
DO - 10.1016/j.jlamp.2015.12.001
M3 - Article
SN - 2352-2208
VL - 85
SP - 269
EP - 286
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
IS - 2
ER -