Scholarlink

<p>The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with various decision procedures and extensions developed for it. However, recent contributions suggest that developing tailored reasoning for some theories, such as sequences and strings, can be more efficient than reasoning over them through axiomatization over the theory of arrays. In this paper, we are interested in reasoning over <InlineEquation ID="IEq4"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="236_2025_496_Article_IEq4.gif" Format="GIF" Height="10" Rendition="HTML" Resolution="72" Type="Linedraw" Width="14" /> </InlineMediaObject> <EquationSource Format="TEX">\(n\)</EquationSource> </InlineEquation>-indexed sequences as they are found in some programming languages, such as Ada. We propose an SMT theory of <InlineEquation ID="IEq5"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="236_2025_496_Article_IEq4.gif" Format="GIF" Height="10" Rendition="HTML" Resolution="72" Type="Linedraw" Width="14" /> </InlineMediaObject> <EquationSource Format="TEX">\(n\)</EquationSource> </InlineEquation>-indexed sequences and explore different ways to represent and reason over <InlineEquation ID="IEq6"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="236_2025_496_Article_IEq4.gif" Format="GIF" Height="10" Rendition="HTML" Resolution="72" Type="Linedraw" Width="14" /> </InlineMediaObject> <EquationSource Format="TEX">\(n\)</EquationSource> </InlineEquation>-indexed sequences using existing theories, as well as tailored calculi for this theory.</p>

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

Reasoning over n-indexed sequences in SMT

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年8月21日

查看全文
  • Hichem Rami Ait-El-Hara,
  • François Bobot,
  • Guillaume Bury

摘要

The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with various decision procedures and extensions developed for it. However, recent contributions suggest that developing tailored reasoning for some theories, such as sequences and strings, can be more efficient than reasoning over them through axiomatization over the theory of arrays. In this paper, we are interested in reasoning over \(n\) -indexed sequences as they are found in some programming languages, such as Ada. We propose an SMT theory of \(n\) -indexed sequences and explore different ways to represent and reason over \(n\) -indexed sequences using existing theories, as well as tailored calculi for this theory.