A Modal-Layered Resolution Calculus for K

2015 ◽  
pp. 185-200 ◽  
Author(s):  
Cláudia Nalon ◽  
Ullrich Hustadt ◽  
Clare Dixon
Keyword(s):  
Resolution Calculus

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).

Complexity of translations from resolution to sequent calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1061-1091
Author(s):  
GISELLE REIS ◽  
BRUNO WOLTZENLOGEL PALEO
Keyword(s):  
Automated Reasoning ◽  
Theoretical Basis ◽  
Automated Theorem Proving ◽  
Proof Theory ◽  
Sequent Calculus ◽  
Formal Proof ◽  
Human Beings ◽  
Proof Systems ◽  
Translation Methods ◽  
Resolution Calculus

Resolution and sequent calculus are two well-known formal proof systems. Their differences make them suitable for distinct tasks. Resolution and its variants are very efficient for automated reasoning and are in fact the theoretical basis of many theorem provers. However, being intentionally machine oriented, the resolution calculus is not as natural for human beings and the input problem needs to be pre-processed to clause normal form. Sequent calculus, on the other hand, is a modular formalism that is useful for analysing meta-properties of various logics and is, therefore, popular among proof theorists. The input problem does not need to be pre-processed, and proofs are more detailed. However, proofs also tend to be larger and more verbose. When the worlds of proof theory and automated theorem proving meet, translations between resolution and sequent calculus are often necessary. In this paper, we compare three translation methods and analyse their complexity.

A Resolution Calculus for Shortening Proofs

2005 ◽  
Vol 13 (3) ◽  
pp. 307-333
Author(s):  
Nicolas Peltier
Keyword(s):  
Resolution Calculus

scholarly journals A resolution calculus for the branching-time temporal logic CTL

2014 ◽  
Vol 15 (1) ◽  
pp. 1-38 ◽  
Author(s):  
Lan Zhang ◽  
Ullrich Hustadt ◽  
Clare Dixon
Keyword(s):  
Temporal Logic ◽  
Branching Time ◽  
Resolution Calculus

scholarly journals A Resolution Calculus for Second-order Logic with Eager Unification

10.29007/zpg2 ◽  
2018 ◽  
Author(s):  
Alexander Leitsch ◽  
Tomer Libal
Keyword(s):  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Unification Algorithm ◽  
Efficient Search ◽  
First Order ◽  
Unification Algorithms ◽  
Second Order Logic ◽  
Resolution Calculus

The efficiency of the first-order resolution calculus is impaired when lifting it to higher-order logic. The main reason for that is the semi-decidability and infinitary natureof higher-order unification algorithms, which requires the integration of unification within the calculus and results in a non-efficient search for refutations.We present a modification of the constrained resolution calculus (Huet'72) which uses an eager unification algorithm while retaining completeness. Thealgorithm is complete with regard to bounded unification only, which for many cases, does not pose a problem in practice.

Sign in / Sign up

Export Citation Format

Share Document