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 条
  • [41] DNA EVIDENCE IN JURY TRIALS: THE "CSI EFFECT"
    Scott, Russ
    JOURNAL OF LAW AND MEDICINE, 2010, 18 (02) : 239 - 259
  • [42] SNOLAB: A Progress Report on the New International Facility for Astroparticle Physics
    Noble, A. J.
    INTERSECTIONS OF PARTICLE AND NUCLEAR PHYSICS, 2009, 1182 : 240 - 243
  • [43] Library Cooperation in Metropolitan New York: Report of Work in Progress
    Gelfand, Morris A.
    COLLEGE & RESEARCH LIBRARIES, 1950, 11 (03): : 245 - 249
  • [44] A New Superconducting Linac for the Nuclotron–NICA Facility: Progress Report
    Bakinovskaya A.A.
    Baturitsky M.A.
    Bakhareva T.A.
    Butenko A.V.
    Gusarova M.A.
    Demyanov S.E.
    Emelyanov N.E.
    Zalessky V.G.
    Zvyagintsev V.L.
    Karpovich V.A.
    Kulevoy T.V.
    Kuraev A.A.
    Lalayan M.V.
    Lozeev Y.Y.
    Maksimenko S.A.
    Matveenko V.V.
    Matsievsky S.V.
    Petrakovsky V.S.
    Pobol I.L.
    Pokrovsky A.I.
    Polozov S.M.
    Pronikov A.I.
    Rak A.
    Rodionova V.N.
    Samoshin A.V.
    Sidorin A.O.
    Sobenin N.P.
    Surkov D.V.
    Syresin E.M.
    Taletsky K.V.
    Trubnikov G.V.
    Shatokhin V.L.
    Shparlo D.A.
    Yurevich S.V.
    Physics of Particles and Nuclei Letters, 2018, 15 (7) : 831 - 834
  • [45] RESEARCH ON POSITION OF NEW-CALEDONIAN LANGUAGES - PROGRESS REPORT
    GRACE, GW
    ASIAN PERSPECTIVES, 1975, 18 (01) : 100 - 100
  • [46] USE OF HEROIN AND METHADONE BY INJECTION IN A NEW TOWN - PROGRESS REPORT
    RATHOD, NH
    BRITISH JOURNAL OF ADDICTION, 1972, 67 (02): : 113 - &
  • [47] PROGRESS REPORT ON THE STATUS OF A NEW DISEASE OF AMERICAN CATS - CYTAUXZOONOSIS
    FERRIS, DH
    COMPARATIVE IMMUNOLOGY MICROBIOLOGY AND INFECTIOUS DISEASES, 1979, 1 (04) : 269 - 276
  • [48] NEW-BRITISH-INTELLIGENCE-SCALE - BRIEF PROGRESS REPORT
    WARD, J
    JOURNAL OF SCHOOL PSYCHOLOGY, 1972, 10 (03) : 307 - 313
  • [49] Validation of new aromatase monoclonal antibodies for immunohistochemistry: progress report
    Sasano, H
    Edwards, DP
    Anderson, TJ
    Silverberg, SG
    Evans, DB
    Santen, RJ
    Ramage, P
    Simpson, ER
    Bhatnagar, AS
    Miller, WR
    JOURNAL OF STEROID BIOCHEMISTRY AND MOLECULAR BIOLOGY, 2003, 86 (3-5): : 239 - 244
  • [50] PROGRESS REPORT ON SEWER RENTAL FOR NEW-YORK-CITY
    GOULD, RH
    SEWAGE AND INDUSTRIAL WASTES, 1951, 23 (07): : 849 - 852
12345