We study quantified propositional logics from the complexity theoretic point of view. First we introduce alternating dependency quantified boolean formulae (ADQBF) which generalize both quantified and dependency quantified boolean formulae. We show that the truth evaluation for ADQBF is AEXPTIME(poly)-complete. We also identify fragments for which the problem is complete for the levels of the exponential hierarchy. Second we study propositional team-based logics. We show that DQBF formulae correspond naturally to quantified propositional dependence logic and present a general NEXPTIME upper bound for quantified propositional logic with a large class of generalized dependence atoms. Moreover we show AEXPTIME(poly)-completeness for extensions of propositional team logic with generalized dependence atoms.
Modal logics allow reasoning about various modes of truth: for example, what it means for something to be possibly true, or to know that something is true as opposed to merely believing it. This report describes embeddings of propositional and quantified modal logic in the PVS verification system. The resources of PVS allow this to be done in an attractive way that supports much of the standard syntax of modal logic, while providing effective automation. The report introduces and formally specifies and verifies several standard topics in modal logic such as relationships between the standard m…
In this paper, we develop a quantified propositional proof systems that corresponds to logarithmic-space reasoning. We begin by defining a class SigmaCNF(2) of quantified formulas that can be evaluated in log space. Then our new proof system GL^* is defined as G_1^* with cuts restricted to SigmaCNF(2) formulas and no cut formula that is not quantifier free contains a free variable that does not appear in the final formula. To show that GL^* is strong enough to capture log space reasoning, we translate theorems of VL into a family of tautologies that have polynomial-size GL^* proofs. VL is a th…
While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynom…
Counting propositional logic was recently introduced in relation to randomized computation and shown able to logically characterize the full counting hierarchy. In this paper we aim to clarify the intuitive meaning and expressive power of its univariate fragment. On the one hand, we provide an effective procedure to measure the probability of counting formulas. On the other, we make the connection between this logic and stochastic experiments explicit, proving that the counting language can simulate any (and only) event associated with dyadic distributions.
In a modular approach, we lift Hilbert-style proof systems for propositional, modal and first-order logic to generalized systems for their respective team-based extensions. We obtain sound and complete axiomatizations for the dependence-free fragment FO(~) of Väänänen's first-order team logic TL, for propositional team logic PTL, quantified propositional team logic QPTL, modal team logic MTL, and for the corresponding logics of dependence, independence, inclusion and exclusion. As a crucial step in the completeness proof, we show that the above logics admit, in a particular sense, a semantics-…
While symmetries are well understood for Boolean formulas and successfully exploited in practical SAT solving, less is known about symmetries in quantified Boolean formulas (QBF). There are some works introducing adaptions of propositional symmetry breaking techniques, with a theory covering only very specific parts of QBF symmetries. We present a general framework that gives a concise characterization of symmetries of QBF. Our framework naturally incorporates the duality of universal and existential symmetries resulting in a general basis for QBF symmetry breaking.
Plausible reasoning concerns situations whose inherent lack of precision is not quantified; that is, there are no degrees or levels of precision, and hence no use of numbers like probabilities. A hopefully comprehensive set of principles that clarifies what it means for a formal logic to do plausible reasoning is presented. A new propositional logic, called Propositional Plausible Logic (PPL), is defined and applied to some important examples. PPL is the only non-numeric non-monotonic logic we know of that satisfies all the principles and correctly reasons with all the examples. Some important…
We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagner's counting hierarchy, but also that the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is derived in the spirit of the Curry-Howard correspondence, showing the potential of counting propositional logic as a useful tool in several fields of theoretical computer science.
Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications which can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, research focused on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula), while non-prenex DQBFs have almost not been studied in the literature. I…
Temporal logics stands for a widely adopted family of formalisms for the verification of computational devices, enriching propositional logics by operators predicating on the step-wise behaviour of a system. Its quantified extensions allow to reason on the properties of the individual components of the system at hand. The expressiveness of the resulting logics poses problems in correctly identifying a semantics that exploit its features without resorting to the imposition of restrictions on the acceptable behaviours. In this paper we address this issue by means of counterpart models and relati…
Prolog is a well known declarative programming language based on propositional Horn formulas. It is useful in various areas, including artificial intelligence, automated theorem proving, mathematical logic and so on. An active research area for many years is to extend Prolog to larger classes of logic. Some important extensions of it includes the constraint logic programming, and the object oriented logic programming. However, it cannot solve problems having arbitrary quantified Horn formulas. To be precise, the facts, rules and queries in Prolog are not allowed to have arbitrary quantified va…
We conceptualize explainability in terms of logic and formula size, giving a number of related definitions of explainability in a very general setting. Our main interest is the so-called special explanation problem which aims to explain the truth value of an input formula in an input model. The explanation is a formula of minimal size that (1) agrees with the input formula on the input model and (2) transmits the involved truth value to the input formula globally, i.e., on every model. As an important example case, we study propositional logic in this setting and show that the special explaina…
Indian Institute of Technology Kanpur（印度理工学院坎普尔分校）；National University of Singapore（新加坡国立大学）
Quantified Boolean Formulas (QBF) extend propositional logic with quantification $\forall, \exists$. In QBF, an existentially quantified variable is allowed to depend on all universally quantified variables in its scope. Dependency Quantified Boolean Formulas (DQBF) restrict the dependencies of existentially quantified variables. In DQBF, existentially quantified variables have explicit dependencies on a subset of universally quantified variables called Henkin dependencies. Given a Boolean specification between the set of inputs and outputs, the problem of Henkin synthesis is to synthesize eac…
In 1978, Schaefer proved his famous dichotomy theorem for generalized satisfiability problems. He defined an infinite number of propositional satisfiability problems, showed that all these problems are either in P or NP-complete, and gave a simple criterion to determine which of the two cases holds. This result is surprising in light of Ladner's theorem, which implies that there are an infinite number of complexity classes between P and NP-complete (under the assumption that P is not equal to NP). Schaefer also stated a dichotomy theorem for quantified generalized Boolean formulas, but this th…
Many verification and synthesis approaches rely on solving techniques for quantified Boolean formulas (QBF). Consequently, solution witnesses, in the form of Boolean functions, become more and more important as they represent implementations or counterexamples. We present a recursive counterexample guided abstraction and refinement algorithm (CEGAR) for solving and certifying QBFs that exploits structural reasoning on the formula level. The algorithm decomposes the given QBF into one propositional formula for every block of quantifiers that abstracts from assignments of variables not bound by …
A quantified Boolean formula (QBF) is a propositional formula extended with universal and existential quantification over propositions. There are two methodologies in CEGAR based QBF solving techniques, one that is based on a refinement loop that builds partial expansions and a more recent one that is based on the communication of satisfied clauses. Despite their algorithmic similarity, their performance characteristics in experimental evaluations are very different and in many cases orthogonal. We compare those CEGAR approaches using proof theory developed around QBF solving and present a uni…
We revisit the notion of intuitionistic equivalence and formal proof representations by adopting the view of formulas as exponential polynomials. After observing that most of the invertible proof rules of intuitionistic (minimal) propositional sequent calculi are formula (i.e. sequent) isomorphisms corresponding to the high-school identities, we show that one can obtain a more compact variant of a proof system, consisting of non-invertible proof rules only, and where the invertible proof rules have been replaced by a formula normalisation procedure. Moreover, for certain proof systems such as …
In spite of the close connection between the evaluation of quantified Boolean formulas (QBF) and propositional satisfiability (SAT), tools and techniques which exploit structural properties of SAT instances are known to fail for QBF. This is especially true for the structural parameter treewidth, which has allowed the design of successful algorithms for SAT but cannot be straightforwardly applied to QBF since it does not take into account the interdependencies between quantified variables. In this work we introduce and develop dependency treewidth, a new structural parameter based on treewidth…
Modal dependence logic was introduced recently by Väänänen. It enhances the basic modal language by an operator =(). For propositional variables p_1,...,p_n, =(p_1,...,p_(n-1);p_n) intuitively states that the value of p_n is determined by those of p_1,...,p_(n-1). Sevenster (J. Logic and Computation, 2009) showed that satisfiability for modal dependence logic is complete for nondeterministic exponential time. In this paper we consider fragments of modal dependence logic obtained by restricting the set of allowed propositional connectives. We show that satisfibility for poor man's dependence lo…
Over the last two decades, propositional satisfiability (SAT) has become one of the most successful and widely applied techniques for the solution of NP-complete problems. The aim of this paper is to investigate theoretically how Sat can be utilized for the efficient solution of problems that are harder than NP or co-NP. In particular, we consider the fundamental reasoning problems in propositional disjunctive answer set programming (ASP), Brave Reasoning and Skeptical Reasoning, which ask whether a given atom is contained in at least one or in all answer sets, respectively. Both problems are …
One of Courcelle's celebrated results states that if C is a class of graphs of bounded tree-width, then model-checking for monadic second order logic is fixed-parameter tractable on C by linear time parameterised algorithms. An immediate question is whether this is best possible or whether the result can be extended to classes of unbounded tree-width. In this paper we show that in terms of tree-width, the theorem can not be extended much further. More specifically, we show that if C is a class of graphs which is closed under colourings and satisfies certain constructibility conditions such tha…
The minimization of propositional formulae is a classical problem in logic, whose first algorithms date back at least to the 1950s with the works of Quine and Karnaugh. Most previous work in the area has focused on obtaining minimal, or quasi-minimal, formulae in conjunctive normal form (CNF) or disjunctive normal form (DNF), with applications in hardware design. In this paper, we are interested in the problem of obtaining an equivalent formula in any format, also allowing connectives that are not present in the original formula. We are primarily motivated in applying minimization algorithms t…
