Proof complexity of modal resolution
From MaRDI portal
Publication:832717
DOI10.1007/s10817-021-09609-9OpenAlexW3207193219MaRDI QIDQ832717
Sarah Sigley, Olaf Beyersdorff
Publication date: 25 March 2022
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-021-09609-9
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Solving QBF with counterexample guided refinement
- Towards NP-P via proof complexity and search
- On the power of clause-learning SAT solvers as resolution engines
- Proof complexity of propositional default logic
- On lengths of proofs in non-classical logics
- Substitution Frege and extended Frege proof systems in non-classical logics
- The intractability of resolution
- Modal resolution in clausal form
- A resolution-based calculus for preferential logics
- A benchmark method for the propositional modal logics K, KT, S4
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- A game characterisation of tree-like Q-resolution size
- Resolution with order and selection for hybrid logics
- A characterization of tree-like resolution size
- On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
- Resolution in Modal, Description and Hybrid Logic
- A resolution-based calculus for Coalition Logic
- Parameterized Bounded-Depth Frege Is not Optimal
- Propositional SAT Solving
- The Complexity of Theorem Proving in Circumscription and Minimal Entailment
- A Modal-Layered Resolution Calculus for K
- Proof-complexity results for nonmonotonic reasoning
- On the correspondence between arithmetic theories and propositional proof systems – a survey
- Polynomial size proofs of the propositional pigeonhole principle
- The relative efficiency of propositional proof systems
- Sequent Calculi for Normal Modal Propositional Logics
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Short proofs are narrow—resolution made simple
- Are Short Proofs Narrow? QBF Resolution Is Not So Simple
- Proof Complexity
- Modal Resolution
- Frege Systems for Quantified Boolean Logic
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- New Resolution-Based QBF Calculi and Their Proof Complexity
- Clique is hard on average for regular resolution
- The Complexity of Theorem Proving in Autoepistemic Logic
- Logical Foundations of Proof Complexity
- Lower bounds for modal logics
- Clausal resolution for normal modal logics
- The Complexity of Propositional Proofs
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- Parameterized Complexity of DPLL Search Procedures
- Proof Complexity of Non-classical Logics
This page was built for publication: Proof complexity of modal resolution
