Linear higher-order pre-unification

被引：5
|
作者：
Cervesato, I
Pfenning, F
机构：
来源：
12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS | 1997年
关键词：
D O I：
10.1109/LICS.1997.614967
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We develop an efficient representation and a pre-unification algorithm in the style of Huet for the linear lambda-calculus lambda(-->-O&T) which includes intuitionistic functions (-->), linear functions (-o), additive pairing (&), and additive unit (T). Applications lie in proof search, logic programming, and logical frameworks based on linear type theories. We also show that, surprisingly, a similar pre-unification algorithm does not exist for certain sublanguages.
引用
收藏
页码：422 / 433
页数：12
相关论文
共 50 条
  • [1] Unification of higher-order patterns in linear time and space
    Qian, Z
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 1996, 6 (03) : 315 - 341
  • [2] Higher-Order Pattern Anti-Unification in Linear Time
    Baumgartner, Alexander
    Kutsia, Temur
    Levy, Jordi
    Villaret, Mateu
    [J]. JOURNAL OF AUTOMATED REASONING, 2017, 58 (02) : 293 - 310
  • [3] Deaccenting and higher-order unification
    Gardent C.
    [J]. Journal of Logic, Language and Information, 2000, 9 (3) : 313 - 338
  • [4] Corrections and higher-order unification
    Gardent, C
    Kohlhase, M
    van Leusen, N
    [J]. NATURAL LANGUAGE PROCESSING AND SPEECH TECHNOLOGY: RESULTS OF THE 3RD KONVENS CONFERENCE, 1996, : 268 - 279
  • [5] Higher-Order Pattern Anti-Unification in Linear Time
    Alexander Baumgartner
    Temur Kutsia
    Jordi Levy
    Mateu Villaret
    [J]. Journal of Automated Reasoning, 2017, 58 : 293 - 310
  • [6] Ramified higher-order unification
    GoubaultLarrecq, J
    [J]. 12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1997, : 410 - 421
  • [7] Piedmont Risorgimento in the pre-unification period
    Bacchin, E.
    [J]. ENGLISH HISTORICAL REVIEW, 2017, 132 (559) : 1617 - 1619
  • [8] HIGHER-ORDER UNIFICATION VIA COMBINATORS
    DOUGHERTY, DJ
    [J]. THEORETICAL COMPUTER SCIENCE, 1993, 114 (02) : 273 - 298
  • [9] Decidability of bounded higher-order unification
    Schmidt-Schauss, M
    Schulz, KU
    [J]. JOURNAL OF SYMBOLIC COMPUTATION, 2005, 40 (02) : 905 - 954
  • [10] Optimizing higher-order pattern unification
    Pientka, B
    Pfenning, F
    [J]. AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 473 - 487
12345