检索结果-内蒙古大学图书馆

certified First-Order AC-Unification and Applications

JOURNAL OF AUTOMATED REASONING 2024年第4期68卷 25页

作者： Ayala-Rincon, Mauricio Fernandez, Maribel Ferreira Silva, Gabriel Kutsia, Temur Nantes-Sobrinho, Daniele Univ Brasilia Dept Comp Sci Brasilia Brazil Kings Coll London Dept Informat London England Johannes Kepler Univ Linz Dept Informat Linz Austria Imperial Coll Dept Comp London England

AC-unification, i.e., unification modulo Associativity and Commutativity axioms is a key component in rewrite-based programming languages and theorem provers. We have used the PVS proof assistant to specify Stickel's pioneering AC-unification algorithm and proved it to be terminating (using an elaborate lexicographic measure based on Fages' termination proof), sound, and complete. We give a detailed account of the formalisation, including descriptions of the main steps in the proofs of termination, soundness, and completeness;the files that were created along with their hierarchy and size;and a discussion about our design choices, including the consequences of our choice for the grammar of terms. We also discuss applications of the certified AC-unification algorithm, showing how the formalisation could be used as a starting point to formalise more efficient AC-unification algorithms or to test implementations of AC-unification algorithms. This formalisation has been used to obtain a certified nominal AC-matching algorithm. Also, it could serve as a basis to specify a nominal AC-unification algorithm once this open theoretical problem is solved.

关键词： AC-unification PVS certified algorithms Formal methods Interactive theorem proving

来源：评论

学校读者我要写书评

暂无评论

certified simultaneous isotopic approximation of algebraic curves via subdivision ☆

引用

JOURNAL OF SYMBOLIC COMPUTATION 2025年 131卷

作者： Burr, Michael Byrd, Michael Clemson Univ 220 Pkwy Dr Clemson SC 29634 USA

We present a certified algorithm based on subdivision for computing an isotopic approximation to any number of algebraic curves in the plane. Our algorithm is based on the certified curve approximation algorithm of Plantinga and Vegter. The main challenge in this algorithm is to correctly and efficiently identify and isolate all intersections between the curves. To overcome this challenge, we introduce a new and simple test that guarantees the global correctness of our output. A main step in our algorithm for approximating any number of curves is to correctly approximate a pair of curves. In addition to developing the details of this special case, we provide complexity analyses for both the number of steps and the bit-complexity of this algorithm using both worst-case bounds as well as those based on continuous amortization and condition numbers. (c) 2025 Elsevier Ltd. All rights are reserved, including those for text and data mining, AI training, and similar technologies.

关键词： Curve approximation Topological correctness certified algorithms Symbolic-numeric algorithms Worst-case bounds Adaptive bounds

来源：评论

学校读者我要写书评

暂无评论

certified simultaneous isotopic approximation of pairs of curves via subdivision 23

Certified simultaneous isotopic approximation of pairs of cu...

引用

48th International Symposium on Symbolic and Algebraic Computation (ISSAC)

作者： Burr, Michael Byrd, Michael Clemson Univ Clemson SC 29634 USA

ISBN: (纸本)9798400700392

We present a certified algorithm based on subdivision for computing an isotopic approximation to a pair of curves in the plane. Our algorithm is based on the certified curve approximation algorithm of Plantinga and Vegter. The main challenge in this computation is to correctly and efficiently compute the intersections of the curves. To address this issue, we introduce a new, but simple test that guarantees the global correctness of our output.

关键词： Pairwise curve approximation Plantinga and Vegter approximation algorithm topological correctness certified algorithms interval arithmetic

来源：评论

学校读者我要写书评

暂无评论

Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration 29th

Certificates for Probabilistic Pushdown Automata via Optimis...

引用

29th International Conference on Tools and algorithms for the Construction and Analysis of Systems (TACAS)

作者： Winkler, Tobias Katoen, Joost-Pieter Rhein Westfal TH Aachen Aachen Germany

ISBN: (纸本)9783031308192;9783031308208

Probabilistic pushdown automata (pPDA) are a standard model for discrete probabilistic programs with procedures and recursion. In pPDA, many quantitative properties are characterized as least fixpoints of polynomial equation systems. In this paper, we study the problem of certifying that these quantities lie within certain bounds. To this end, we first characterize the polynomial systems that admit easy-to-check certificates for validating bounds on their least fixpoint. Second, we present a sound and complete Optimistic Value Iteration algorithm for computing such certificates. Third, we show how certificates for polynomial systems can be transferred to certificates for various quantitative pPDA properties. Experiments demonstrate that our algorithm computes succinct certificates for several intricate example programs as well as stochastic context-free grammars with > 10(4) production rules.

关键词： Probabilistic Pushdown Automata Probabilistic Model Checking certified algorithms Probabilistic Recursive Programs

来源：评论

学校读者我要写书评

暂无评论

certified Bit-Coded Regular Expression Parsing 17

Certified Bit-Coded Regular Expression Parsing

引用

21st Brazilian Symposium on Programming Languages (SBLP) as Part of 8th Brazilian Conference on Software (CBSoft)

作者： Ribeiro, Rodrigo Du Bois, Andre Univ Fed Ouro Preto Ouro Preto MG Brazil Univ Fed Pelotas Pelotas RS Brazil

ISBN: (纸本)9781450353892

We describe the formalization of a regular expression (RE) parsing algorithm that produces a bit representation of its parse tree in the dependently typed language Agda. The algorithm computes bit-codes using Brzozowski derivatives and we prove that produced codes are equivalent to parse trees ensuring soundness and completeness w.r.t an inductive RE semantics. We include the certified algorithm in a tool developed by us, named verigrep, for regular expression based search in the style of the well known GNU grep. Practical experiments conducted with this tool are reported.

关键词： certified algorithms regular expressions bit-codes dependent types

来源：评论

学校读者我要写书评

暂无评论

From Certification of algorithms to certified MPC: The Missing Links

引用

IFAC-PapersOnLine 2015年第23期48卷 65-72页

作者： Alamir, Mazen Gipsa-lab CNRS-Control Systems Department University of Grenoble France

Deriving certification bounds for optimization algorithms is an active research area in the control community. This is mainly impulsed by the use of on-line optimization algorithms in real-time MPC through limited computation power. However, the way such bounds are then used to derive a convergence certification for MPC frameworks is still not suficiently mature. This paper contributes in clarifying what are the unavoidable additional ingredients that need to be combined with any algorithm's certification bound in order to derive a relevant certification result for the MPC-based closed-loop performance. Moreover, the paper gives such a general certification result based on these ingredients for any pair of certified algorithm and provably stable ideal MPC formulation. The proposed framework is then instantiated to the particular case of linear MPC and a simple example is given to illustrate the introduced concepts. © 2015, IFAC (International Federation of Automatic Control) Hosting by Elsevier Ltd. All rights reserved.

关键词： Optimization Real time control certified algorithms Closed loop performance Computation power MPC Certification Online optimization Optimization algorithms Real time implementations State dependent

来源：评论

学校读者我要写书评

暂无评论

On the Complexity of Solving Zero-Dimensional Polynomial Systems via Projection 16

On the Complexity of Solving Zero-Dimensional Polynomial Sys...

引用

41st ACM International Symposium on Symbolic and Algebraic Computation (ISSAC)

作者： Brand, Cornelius Sagraloff, Michael Univ Saarland Cluster Excellence MMCI Campus E17 D-66123 Saarbrucken Germany Max Planck Inst Informat Campus E14 D-66123 Saarbrucken Germany

ISBN: (纸本)9781450343800

Given a zero-dimensional polynomial system consisting of n integer polynomials in n variables, we propose a certified and complete method to compute all complex solutions of the system as well as a corresponding separating linear form 1 with coefficients of small bit size. For computing 1, we need to project the solutions into one dimension along 0(n) distinct directions but no further algebraic manipulations. The solutions are then directly reconstructed from the considered projections. The first step is deterministic, whereas the second step uses randomization, thus being Las-Vegas. The theoretical analysis of our approach shows that the overall cost for the two problems considered above is dominated by the cost of carrying out the projections. We also give bounds on the bit complexity of our algorithms that are exclusively stated in terms of the number of variables, the total degree and the bitsize of the input polynomials.

关键词： polynomial system solving bit complexity certified algorithms resultant computation separating form

来源：评论

学校读者我要写书评

暂无评论

certified Numerical Homotopy Tracking

引用

EXPERIMENTAL MATHEMATICS 2012年第1期21卷 69-83页

作者： Beltran, Carlos Leykin, Anton Univ Cantabria Dept Matemat Estadist & Computac Cantabria Spain Georgia Tech Sch Math Atlanta GA USA

Given a homotopy connecting two polynomial systems, we provide a rigorous algorithm for tracking a regular homotopy path connecting an approximate zero of the start system to an approximate zero of the target system. Our method uses recent results on the complexity of homotopy continuation rooted in the alpha theory of Smale. Experimental results obtained with an implementation in the numerical algebraic geometry package Macaulay2 demonstrate the practicality of the algorithm. In particular, we confirm the theoretical results for random linear homotopies and illustrate the plausibility of a conjecture by Shub and Smale on a good initial pair.

关键词： Computational aspects of algebraic geometry systems of equations continual methods homotopy methods approximate zero certified algorithms complexity

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：