scientific article; zbMATH DE number 7029311
From MaRDI portal
Publication:4625701
Lorenzo Clemente, Richard Mayr
Publication date: 25 February 2019
Full work available at URL: https://arxiv.org/abs/1711.09946
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Simplifying regular expressions further, On minimizing regular expressions without Kleene star, On the decidability of infix inclusion problem, On the power of finite ambiguity in Büchi complementation, Simulation relations and applications in formal methods, Unnamed Item, Nondeterministic syntactic complexity
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Towards NP-P via proof complexity and search
- On the complexity of cutting-plane proofs
- Random CNF's are hard for the polynomial calculus
- A threshold for unsatisfiability
- The intractability of resolution
- The complementation problem for Büchi automata with applications to temporal logic
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
- Understanding cutting planes for QBFs
- Expansion-based QBF solving versus Q-resolution
- Conformant planning as a case study of incremental QBF solving
- Unified QBF certification and its applications
- A characterization of tree-like resolution size
- A Game Characterisation of Tree-like Q-resolution Size
- Lower Bounds
- On Stronger Calculi for QBFs
- Q-Resolution with Generalized Axioms
- Long Distance Q-Resolution with Dependency Schemes
- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
- On Unification of QBF Resolution-Based Calculi
- SAT-Based Synthesis Methods for Safety Specs
- Decidability Results on the Existence of Lookahead Delegators for NFA
- Büchi Store: An Open Repository of Büchi Automata
- Space Complexity in Propositional Calculus
- A new upper bound for 3-SAT
- QBF Resolution Systems and Their Proof Complexities
- Evaluating and certifying QBFs: A comparison of state-of-the-art tools
- Antichain Algorithms for Finite Automata
- When Simulation Meets Antichains
- Efficient Büchi Universality Checking
- Equivalence and Inclusion Problem for Strongly Unambiguous Büchi Automata
- Multipebble Simulations for Alternating Automata
- Fault Localization and Correction with QBF
- Büchi Complementation and Size-Change Termination
- TaPAS: The Talence Presburger Arithmetic Suite
- The relative efficiency of propositional proof systems
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Short proofs are narrow—resolution made simple
- Are Short Proofs Narrow? QBF Resolution Is Not So Simple
- Understanding Gentzen and Frege Systems for QBF
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- Automated Testing and Debugging of SAT and QBF Solvers
- The size-change principle for program termination
- Exact location of the phase transition for random (1,2)-QSAT
- Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds
- What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead
- The Complexity of Propositional Proofs
- Deterministic Simulation of a NFA with k–Symbol Lookahead
- GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
- Theory and Applications of Satisfiability Testing
- Antichains: A New Algorithm for Checking Universality of Finite Automata
- Random 2-SAT: Results and problems
