A comparison of the resolution calculus and the connection method, and a new calculus generalizing both methods

2005 ◽  
pp. 80-98 ◽  
Author(s):  
Elmar Eder
Keyword(s):  
Connection Method ◽  
Resolution Calculus

scholarly journals A Quantum Monte Carlo Approach to the Adiabatic Connection Method

1998 ◽  
pp. 189-207 ◽  
Author(s):  
Maziar Nekovee ◽  
W.M.C. Foulkes ◽  
A.J. Williamson ◽  
G. Rajagopal ◽  
R.J. Needs
Keyword(s):  
Monte Carlo ◽  
Quantum Monte Carlo ◽  
Monte Carlo Approach ◽  
Connection Method

Chapter 29. Theory of Quantified Boolean Formulas

2021 ◽  
Author(s):  
Hans Kleine Büning ◽  
Uwe Bubeck
Keyword(s):  
Normal Form ◽  
Boolean Function ◽  
Expressive Power ◽  
Modeling Language ◽  
Complex Problems ◽  
Quantified Boolean Formulas ◽  
Horn Formulas ◽  
Boolean Formulas ◽  
Function Models ◽  
Resolution Calculus

Quantified Boolean formulas (QBF) are a generalization of propositional formulas by allowing universal and existential quantifiers over variables. This enhancement makes QBF a concise and natural modeling language in which problems from many areas, such as planning, scheduling or verification, can often be encoded in a more compact way than with propositional formulas. We introduce in this chapter the syntax and semantics of QBF and present fundamental concepts. This includes normal form transformations and Q-resolution, an extension of the propositional resolution calculus. In addition, Boolean function models are introduced to describe the valuation of formulas and the behavior of the quantifiers. We also discuss the expressive power of QBF and provide an overview of important complexity results. These illustrate that the greater capabilities of QBF lead to more complex problems, which makes it interesting to consider suitable subclasses of QBF. In particular, we give a detailed look at quantified Horn formulas (QHORN) and quantified 2-CNF (Q2-CNF).

Sign in / Sign up

Export Citation Format

Share Document