Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF [0.03%]
Dependency图释依赖方案：DQBF中的(soundness meets incompleteness).soundness和incompleteness是两个关键词，在这里作为形容词使用，可以翻译为“一致性”与“不完备性”，所以完整的中文标题翻译如下：
重新诠释依赖方案：一致性与不完备性在DQBF中的相互作用
Olaf Beyersdorff,Joshua Blinkhorn,Leroy Chew et al.
Olaf Beyersdorff et al.
Dependency quantified Boolean formulas (DQBF) and QBF dependency schemes have been treated separately in the literature, even though both treatments extend QBF by replacing the linear order of the quantifier prefix with a partial order. We ...
Tomáš Peitl,Friedrich Slivovsky,Stefan Szeider
Tomáš Peitl
Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers that use these systems to generate proofs. We study a combination of two proof ...
Stijn de Gouw,Frank S de Boer,Richard Bubel et al.
Stijn de Gouw et al.
TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we ...
Extraction of Expansion Trees [0.03%]
扩张树的提取
Alexander Leitsch,Anela Lolic
Alexander Leitsch
We define a new method for proof mining by CERES (cut-elimination by resolution) that is concerned with the extraction of expansion trees in first-order logic (see Miller in Stud Log 46(4):347-370, 1987) with equality. In the original CERES...
José Iborra,Naoki Nishida,Germán Vidal et al.
José Iborra et al.
A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times...
Alexander Baumgartner,Temur Kutsia,Jordi Levy et al.
Alexander Baumgartner et al.
We present a rule-based Huet's style anti-unification algorithm for simply typed lambda-terms, which computes a least general higher-order pattern generalization. For a pair of arbitrary terms of the same type, such a generalization always ...
M Ganesalingam,W T Gowers
M Ganesalingam
This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians. ...
Aleksandar Zeljić,Christoph M Wintersteiger,Philipp Rümmer
Aleksandar Zeljić
We consider the problem of automatically and efficiently computing models of constraints, in the presence of complex background theories such as floating-point arithmetic. Constructing models, or proving that a constraint is unsatisfiable, ...
Robbert Krebbers
Robbert Krebbers
The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches the description of C in the C11 standard is challenging bec...
Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs [0.03%]
带标签的超解析、子句式和局部证明插值系统
Matthias Schlaipfer,Georg Weissenbacher
Matthias Schlaipfer
Craig's interpolation theorem has numerous applications in model checking, automated reasoning, and synthesis. There is a variety of interpolation systems which derive interpolants from refutation proofs; these systems are ad-hoc and rigid ...