A First-Order Calculus for Allegories

被引：0
|
作者：
Aameri, Bahar [1 ]
Winter, Michael [2 ]
机构：
[1] Univ Toronto, Dept Comp Sci, Toronto, ON M5S 3G8, Canada
[2] Brock Univ, Dept Comp Sci, St Catharines, ON L2S 3A1, Canada
来源：
RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE | 2011年 / 6663卷
基金：
加拿大自然科学与工程研究理事会;
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper we present a language and first-order calculus for formal reasoning about relations based on the theory of allegories. Since allegories are categories, the language is typed in Church-style. We show soundness and completeness of the calculus and demonstrate its usability by presenting the RelAPS system; a proof assistant for relational categories based on the calculus presented here.
引用
收藏
页码：74 / 91
页数：18
相关论文
共 50 条
  • [21] Proof Search for the First-Order Connection Calculus in Maude
    Holen, Bjarne
    Johnsen, Einar Broch
    Waaler, Arild
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 238 (03) : 173 - 188
  • [22] General models and completeness of first-order modal μ-calculus
    Kashima, Ryo
    Okamoto, Keishi
    JOURNAL OF LOGIC AND COMPUTATION, 2008, 18 (04) : 497 - 507
  • [23] Interpretability of first-order dynamic logic in a relational calculus
    Frias, MF
    Baum, GA
    Maibaum, TSE
    RELATIONAL METHODS IN COMPUTER SCIENCE, 2002, 2561 : 66 - 80
  • [24] The model evolution calculus as a first-order DPLL method
    Baumgartner, Peter
    Tinelli, Cesare
    ARTIFICIAL INTELLIGENCE, 2008, 172 (4-5) : 591 - 632
  • [25] Soundness of First-order Fuzzy Predicate Calculus System
    Zhao Zheng-bo
    2012 INTERNATIONAL CONFERENCE ON FUTURE INFORMATION TECHNOLOGY AND MANAGEMENT SCIENCE & ENGINEERING (FITMSE 2012), 2012, 14 : 47 - 52
  • [26] Rewriting calculus with fixpoints: Untyped and first-order systems
    Cirstea, H
    Liquori, L
    Wack, B
    TYPES FOR PROOFS AND PROGRAMS, 2004, 3085 : 147 - 161
  • [27] First-order μ-calculus over generic transition systems and applications to the situation calculus
    Calvanese, Diego
    De Giacomo, Giuseppe
    Montali, Marco
    Patrizi, Fabio
    INFORMATION AND COMPUTATION, 2018, 259 : 328 - 347
  • [28] Remarks on Functional Calculus for Perturbed First-order Dirac Operators
    Auscher, Pascal
    Stahlhut, Sebastian
    OPERATOR THEORY IN HARMONIC AND NON-COMMUTATIVE ANALYSIS, 2014, 240 : 31 - 43
  • [29] ALEPHO0-CATEGORICITY IN FIRST-ORDER PREDICATE CALCULUS
    FUHRKEN, G
    JOURNAL OF SYMBOLIC LOGIC, 1966, 31 (03) : 504 - +
  • [30] A linear translation from CTL* to the first-order modal μ-calculus
    Cranen, Sjoerd
    Groote, Jan Friso
    Reniers, Michel
    THEORETICAL COMPUTER SCIENCE, 2011, 412 (28) : 3129 - 3139
12345