Collections, Cardinalities and Relations

被引:0
|
作者
Yessenov, Kuat [1 ]
Piskac, Ruzica [2 ]
Kuncak, Viktor [2 ]
机构
[1] MIT, Comp Sci & Artificial Intelligence Lab, Cambridge, MA 02139 USA
[2] Ecole Polytech Fed Lausanne, Sch Comp & Commun Sci, CH-1015 Lausanne, Switzerland
基金
瑞士国家科学基金会;
关键词
LOGIC;
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Logics that involve collections (sets, multisets), and cardinality constraints are useful for reasoning about unbounded data structures and concurrent processes. To make such logics more useful in verification this paper extends them with the ability to compute direct and inverse relation and function images. We establish decidability and complexity bounds for the extended logics.
引用
收藏
页码:380 / +
页数:3
相关论文
共 50 条
  • [1] Cardinalities of Finite Relations in Coq
    Brunet, Paul
    Pous, Damien
    Stucke, Insa
    [J]. INTERACTIVE THEOREM PROVING (ITP 2016), 2016, 9807 : 466 - 474
  • [2] Relations between cardinalities of the finite sequences and the finite subsets of a set
    Aksornthong, Navin
    Vejjajiva, Pimpen
    [J]. MATHEMATICAL LOGIC QUARTERLY, 2018, 64 (06) : 529 - 534
  • [3] Linear Algebraic Relations among Cardinalities of Sets of Matroid Functions
    Kochol, Martin
    [J]. MATHEMATICS, 2023, 11 (11)
  • [4] Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants
    Stucke, Insa
    [J]. RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE, RAMICS 2017, 2017, 10226 : 290 - 306
  • [5] CARDINALITIES OF A + A AND A - A
    STEIN, SK
    [J]. CANADIAN MATHEMATICAL BULLETIN-BULLETIN CANADIEN DE MATHEMATIQUES, 1973, 16 (03): : 343 - 345
  • [6] CARDINALITIES OF A + A AND A - A
    STEIN, SK
    [J]. NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1972, 19 (01): : A3 - &
  • [7] A Bundle of Relations: Collections, Collecting, and Communities
    Bell, Joshua A.
    [J]. ANNUAL REVIEW OF ANTHROPOLOGY, VOL 46, 2017, 46 : 241 - 259
  • [8] ON CARDINALITIES OF ULTRAPRODUCTS
    KEISLER, HJ
    [J]. BULLETIN OF THE AMERICAN MATHEMATICAL SOCIETY, 1964, 70 (04) : 644 - &
  • [9] Brouwer and cardinalities
    Hart, Klaas Pieter
    [J]. INDAGATIONES MATHEMATICAE-NEW SERIES, 2018, 29 (06): : 1555 - 1564
  • [10] ON ORDERING OF CARDINALITIES
    JECH, T
    [J]. BULLETIN DE L ACADEMIE POLONAISE DES SCIENCES-SERIE DES SCIENCES MATHEMATIQUES ASTRONOMIQUES ET PHYSIQUES, 1966, 14 (06): : 293 - &