Anthony Bordg,Hanna Lachnitt,Yijun He
Anthony Bordg
In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and proto...
Pascal Fontaine
Pascal Fontaine
Michael Färber,Cezary Kaliszyk,Josef Urban
Michael Färber
Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: first, we show optimised functional implementations of connection tableaux proo...
Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration [0.03%]
基于抽象加速的带输入有界时间LTI系统安全验证
Dario Cattaruzza,Alessandro Abate,Peter Schrammel et al.
Dario Cattaruzza et al.
Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses ...
Olaf Beyersdorff,Joshua Blinkhorn,Meena Mahajan
Olaf Beyersdorff
Strategy extraction is of great importance for quantified Boolean formulas (QBF), both in solving and proof complexity. So far in the QBF literature, strategy extraction has been algorithmically performed from proofs. Here we devise the fir...
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL [0.03%]
Isabelle / HOL中的LLL基础约简算法及因式分解算法的形式化
René Thiemann,Ralph Bottesch,Jose Divasón et al.
René Thiemann et al.
The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely...
A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm [0.03%]
形式化验证的Berlekamp-Zassenhaus整系数多项式分裂算法的实现与证明
Jose Divasón,Sebastiaan J C Joosten,René Thiemann et al.
Jose Divasón et al.
We formally verify the Berlekamp-Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun's square-free factorization algorithm to integer polynomials, and thus pr...
Marijn J H Heule,Benjamin Kiesl,Armin Biere
Marijn J H Heule
We introduce proof systems for propositional logic that admit short proofs of hard formulas as well as the succinct expression of most techniques used by modern SAT solvers. Our proof systems allow the derivation of clauses that are not nec...
Sebastiaan J C Joosten,René Thiemann,Akihisa Yamada
Sebastiaan J C Joosten
We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of ratio...
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL [0.03%]
通过Isabelle / HOL中的柯西指标评估缠绕数和计算复根
Wenda Li,Lawrence C Paulson
Wenda Li
In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover,...