Scholarlink

We discuss a technique, based on Angluin’s algorithm, for automatically generating finite automata for various kinds of useful first-order logic formulas in Büchi arithmetic. Construction in this way can be faster and use much less space than more direct methods. We discuss the theory and we present some empirical data for the free software Walnut.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Self-verifying Predicates in Büchi Arithmetic

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Mazen Khodier,
  • Luke Schaeffer,
  • Jeffrey Shallit

摘要

We discuss a technique, based on Angluin’s algorithm, for automatically generating finite automata for various kinds of useful first-order logic formulas in Büchi arithmetic. Construction in this way can be faster and use much less space than more direct methods. We discuss the theory and we present some empirical data for the free software Walnut.