Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers [0.03%]
具有分布式子句共享的SAT解算器的不满足证明生成
Dawn Michaelson,Dominik Schreiber,Marijn J H Heule et al.
Dawn Michaelson et al.
Distributed clause-sharing SAT solvers can solve challenging problems hundreds of times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers. Unlike sequential solvers, however, distributed sol...
Cezary Kaliszyk,Karol Pąk
Cezary Kaliszyk
The Isabelle Higher-order Tarski-Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing the libraries of Isabelle/HOL and Isabelle/Mizar. The two libraries, however, define all t...
Alessandro Abate,Haniel Barbosa,Clark Barrett et al.
Alessandro Abate et al.
Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. Whi...
Unifying Splitting [0.03%]
统一拆分
Gabriel Ebner,Jasmin Blanchette,Sophie Tourret
Gabriel Ebner
AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying ...
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification [0.03%]
线性变量分离重写系统的重写理论：自动化、形式化和验证
Aart Middeldorp,Alexander Lochmann,Fabian Mitterwallner
Aart Middeldorp
The first-order theory of rewriting is decidable for linear variable-separated rewrite systems. We present a new decision procedure which is the basis of FORT, a decision and synthesis tool for properties expressible in the theory. The deci...
Wilmer Ricciotti,James Cheney
Wilmer Ricciotti
SQL is the world's most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specifica...
Uwe Waldmann,Sophie Tourret,Simon Robillard et al.
Uwe Waldmann et al.
A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalenc...
Jose Divasón,René Thiemann
Jose Divasón
This work presents formal correctness proofs in Isabelle/HOL of algorithms to transform a matrix into Smith normal form, a canonical matrix form, in a general setting: the algorithms are written in an abstract form and parameterized by very...
Nicolas Peltier,Viorica Sofronie-Stokkermans
Nicolas Peltier
Sarah Sigley,Olaf Beyersdorff
Sarah Sigley
We investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3-4):117-134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods-24th international confer...