Related Concept Videos
Distance Problem
The Z-Scheme of Electron Transport in Photosynthesis
Distance Corrections
The Distance Formula
Short-distance Transport of Resources
Distance Measurements by Taping
You might also read
Related Articles
Articles linked to this work by shared authors, journal, and citation graph.
From Data Completion to Problems on Hypercubes: A Parameterized Analysis of the Independent Set Problem.
Combining Higher-Order Logic with Set Theory Formalizations.
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification.
A Comprehensive Framework for Saturation Theorem Proving.
Related Experiment Video
Updated: Jan 24, 2026

A High Resolution Method to Monitor Phosphorylation-dependent Activation of IRF3
Published on: January 24, 2016
Long-Distance Q-Resolution with Dependency Schemes.
Tomáš Peitl1, Friedrich Slivovsky1, Stefan Szeider1
1Algorithms and Complexity Group, TU Wien, 1040 Vienna, Austria.
We introduce long-distance Q(D)-resolution, a sound proof system for quantified Boolean formulas (QBFs). This system enables polynomial-time strategy extraction, enhancing the reliability of QBF solvers.
Area of Science:
- Formal verification
- Automated reasoning
- Theoretical computer science
Background:
- Resolution proof systems are crucial for analyzing quantified Boolean formula (QBF) solvers.
- State-of-the-art QBF solvers utilize these systems to generate proofs.
Purpose of the Study:
- To investigate a novel proof system combining Q-resolution with generalized universal reduction and long-distance Q-resolution.
- To establish the soundness and efficiency of this new system for QBF solving.
Main Methods:
- Combining Q-resolution with generalized universal reduction and long-distance Q-resolution.
- Developing a general result for polynomial-time strategy extraction across various dependency schemes.
- Analyzing the proof generation process of search-based QBF solvers.
Main Results:
- Introduced long-distance Q(D)-resolution, a sound proof system for reflexive resolution-path dependency schemes.
- Demonstrated polynomial-time strategy extraction for long-distance Q(D)-resolution under a broad class of dependency schemes.
- Showed that search-based QBF solvers with learning generate long-distance Q(D)-resolution proofs, ensuring partial soundness.
Conclusions:
- Long-distance Q(D)-resolution offers enhanced reliability and efficiency for QBF solving.
- The findings provide theoretical underpinnings for improving the performance and trustworthiness of automated QBF solvers.
- Experimental results with DepQBF validate the practical applicability of the developed proof system.

