CSI: New Evidence - A Progress Report

被引：19
|
作者：
Nagele, Julian [1 ]
Felgenhauer, Bertram [1 ]
Middeldorp, Aart [1 ]
机构：
[1] Univ Innsbruck, Dept Comp Sci, Innsbruck, Austria
来源：
AUTOMATED DEDUCTION - CADE 26 | 2017年 / 10395卷
基金：
奥地利科学基金会;
关键词：
ORDER REWRITE SYSTEMS; CONFLUENCE; CERTIFICATION;
D O I：
10.1007/978-3-319-63046-5_24
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
CSI is a strong automated confluence prover for rewrite systems which has been in development since 2010. In this paper we report on recent extensions that make CSI more powerful, secure, and useful. These extensions include improved confluence criteria but also support for uniqueness of normal forms. Most of the implemented techniques produce machine-readable proof output that can be independently verified by an external tool, thus increasing the trust in CSI. We also report on CSI(boolean AND)oho, a tool built on the same framework and similar ideas as CSI that automatically checks confluence of higher-order rewrite systems.
引用
收藏
页码：385 / 397
页数：13
相关论文
共 50 条
  • [1] A progress report on the development of the CsI-RICH detector for the ALICE experiment at LHC
    Beker, H
    Braem, A
    Colonna, N
    Davenport, M
    Di Bari, D
    Di Mauro, A
    Elia, D
    Fini, R
    Galantucci, L
    Ghidini, B
    Goret, B
    Grimaldi, A
    Monno, E
    Nappi, E
    Paic, G
    Piuz, F
    Posa, F
    Raynaud, J
    Santiard, JC
    Stucchi, S
    Tomasicchio, G
    Williams, TD
    NUCLEAR INSTRUMENTS & METHODS IN PHYSICS RESEARCH SECTION A-ACCELERATORS SPECTROMETERS DETECTORS AND ASSOCIATED EQUIPMENT, 1998, 409 (1-3): : 385 - 389
  • [2] THE NEW JOURNAL - PROGRESS REPORT
    SWALES, JD
    TREASURE, T
    JOURNAL OF THE ROYAL SOCIETY OF MEDICINE, 1995, 88 (05) : P277 - P277
  • [3] New steroids for IBD: progress report
    Hanauer, SB
    GUT, 2002, 51 (02) : 182 - 183
  • [4] The New Robotic Telescope: Progress report
    Jermak, Helen E.
    Barrera, Josue
    Copley, David
    Copperwheat, Christopher M.
    De Cos Juez, Javier
    Gracia Rodriquez, Javier
    Fernandez-Valdivia, J. J.
    Pinero, A. Garci A.
    Gutierrez, Carlos M.
    Harvey, Eamonn
    Insausti, Maider
    Knapen, Johan H.
    Maudes Gutierrez, Antonio
    McGrath, Adrian M.
    Oria, Asier
    Ranjbar, Ali
    Rebolo-Lopez, Rafael
    Steele, Iain A.
    Torres, Miguel
    Xu, Dong
    Panyaphirawat, Thirasak
    Aukkaravittayapun, Suparerk
    GROUND-BASED AND AIRBORNE TELESCOPES VIII, 2020, 11445
  • [5] IMPLEMENTING A NEW ELEMENTARY PROGRESS REPORT
    CLARRIDGE, PB
    WHITAKER, EM
    EDUCATIONAL LEADERSHIP, 1994, 52 (02) : 7 - 9
  • [6] NEW YORK NETWORK - A PROGRESS REPORT
    DOHERTY, JW
    JOURNAL OF THE SOCIETY OF MOTION PICTURE TELEVISION ENGINEERS, 1968, 77 (10): : 1043 - &
  • [7] NEW HEALTH PRACTITIONERS - PROGRESS REPORT
    不详
    CONNECTICUT MEDICINE, 1980, 44 (02) : 107 - 110
  • [8] NEW YORK NETWORK - A PROGRESS REPORT
    DOHERTY, JW
    JOURNAL OF THE SOCIETY OF MOTION PICTURE TELEVISION ENGINEERS, 1968, 77 (04): : 392 - &
  • [9] New evidence of generational progress for Mexican Americans
    Duncan, Brian
    Grogger, Jeffrey
    Leon, Ana Sofia
    Trejo, Stephen J.
    LABOUR ECONOMICS, 2020, 62
  • [10] New evidence of progress in the national cancer program
    Mettlin, CJ
    CANCER, 1996, 78 (10) : 2043 - 2044
12345