ACLApr, 2013

ACL2 版本 5.0、6.0 和 6.1 的增强功能

PDF
TL;DR介绍了自 2011 年 ACL2 研讨会以来在 ACL2 版本中引入的增强功能，重点介绍了那些可以使用户受益的改进，但这些改进可能不会在日常实践中被发现。
发现论文，激发创造
  • ACL2 版本 6.2、6.3 和 6.4 的增强功能

    本文介绍了自 2013 年 ACL2 研讨会以来对 ACL2 的改进，并涉及形式验证和定理证明方面的研究领域。

    Jun, 2014

  • ACL2 定理证明器及其应用国际研讨会第十三届会议论文集

    该论文介绍了一个自动化推理系统 ACL2 定理证明器，其应用包括计算系统规范和验证，形式验证等，Boyer-Moore 家族的成员在 ACL2 Theorem Prover 研究和发展中做出重要贡献。

    Sep, 2015

  • ACL2 证明调试工具的进展

    ACL2 用户的经验通常包括许多失败的证明尝试，成功使用 ACL2 prover 的关键在于有效利用调试工具，本文侧重于 ACL2 版本 8.5 之后的改进，包括改进的 break-rewrite 工具和新的 with-brr-data 实用工具。

    Nov, 2023

  • ACL2 定理证明器及其应用国际研讨会第十七届会议论文集

    该论文集收录了 ACL2 定理证明器及其应用方面的研究和经验，讨论 ACL2 定理证明器在技术论坛和应用方面的作用。

    May, 2022

  • ACL 文献数据库的历时研究：自然语言处理文献的现状

    分析了 ACL Anthology 中自然语言处理研究的文献，关注研究的生产力、关注点和影响，特别强调了 NLP 研究出版物的多元化和包容性，并发现只有约 30％的第一作者是女性，并且即使考虑了经验，女性第一作者的引用量也比男性第一作者低。

    Nov, 2019

  • ACL OCL 语料库：推动计算语言学中的开放科学

    ACL OCL 是一个学术语料库，包含了 74k 篇计算语言学领域的科学论文，210k 个提取的图形，以及针对所有 OCL 论文的主题。该研究观察到语法标注、分块和解析主题明显下降，而自然语言生成主题再次兴盛。

    May, 2023

  • TPTP 风格的自动定理证明器在 ACL2 问题上的初步实验

    本文初步探讨了在 ACL2 系统上使用外部 ATP 进行实验的情况，旨在为解决 ACL2 问题提供外部推理和人工智能系统的初步效用评估。

    Jun, 2014

  • ACL 论文助手：从 ACL 文集中检索和管理文献的工具

    这篇论文介绍了一个名为 “ACL Anthology Helper” 的工具，它自动化解析和下载论文及其元信息，并将其存储在本地 MySQL 数据库中，从而实现了对本地论文的高效管理。该工具提供了 20 多种操作，极大地提升了根据特定条件检索文献的能力，并成功应用于撰写了一篇综述论文。通过引入 ACL Anthology Helper，我们旨在提升研究人员有效访问和组织 ACL Anthology 中的文献的能力，为研究人员在探索 ACL Anthology 庞大的出版物集合时提供了便利的解决方案，并允许更有针对性和高效的文献检索。

    Oct, 2023

  • CL Scholar: ACL Anthology 知识图谱挖掘工具

    CL Scholar 是一种基于文本和网络信息构建的 ACL 医学知识图谱挖掘器，支持使用自然语言查询和关键词搜索来精确探索当前计算语言学研究进展。

    Apr, 2018

  • ACL2 (r) 中的凸函数

    本文在 ACL2 (r) 平台上对 R^n 进行了形式化处理，并着重研究了凸函数的一组公理和证明，包括了一组关于引理的等价条件，并且探讨了证明工程的问题。

    Oct, 2018