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 条
  • [1] FIRST-ORDER REGGE CALCULUS
    BARRETT, JW
    CLASSICAL AND QUANTUM GRAVITY, 1994, 11 (11) : 2723 - 2730
  • [2] Cyclic proofs for the first-order μ-calculus
    AFSHARI, B. A. H. A. R. E. H.
    ENQVIST, S. E. B. A. S. T. I. A. N.
    LEIGH, G. R. A. H. A. M. E.
    LOGIC JOURNAL OF THE IGPL, 2024, 32 (01) : 1 - 34
  • [3] A FIRST-ORDER RESOLUTION CALCULUS WITH SYMMETRIES
    EGLY, U
    LOGIC PROGRAMMING AND AUTOMATED REASONING, 1993, 698 : 110 - 121
  • [4] A Sequent Calculus for First-Order Logic
    Braselmann, Patrick
    Koepke, Peter
    FORMALIZED MATHEMATICS, 2005, 13 (01): : 33 - 39
  • [5] First-order constrained lambda calculus
    Crossley, JN
    Mandel, L
    Wirsing, M
    FRONTIERS OF COMBINING SYSTEMS, 1996, 3 : 339 - 356
  • [6] A Resolution Calculus for First-order Schemata
    Aravantinos, Vincent
    Echenim, Mnacho
    Peltier, Nicolas
    FUNDAMENTA INFORMATICAE, 2013, 125 (02) : 101 - 133
  • [7] First-order calculus and option pricing
    Carr, Peter
    INTERNATIONAL JOURNAL OF FINANCIAL ENGINEERING, 2014, 1 (01)
  • [8] On First-Order μ-Calculus over Situation Calculus Action Theories
    Calvanese, Diego
    De Giacomo, Giuseppe
    Montali, Marco
    Patrizi, Fabio
    FIFTEENTH INTERNATIONAL CONFERENCE ON THE PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2016, : 411 - 420
  • [9] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems
    Xian Xu
    Journal of Computer Science and Technology, 2009, 24 : 122 - 137
  • [10] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems
    徐贤
    JournalofComputerScience&Technology, 2009, 24 (01) : 122 - 137
12345