The Kolmogorov Expression Complexity of Logics

The purpose of the paper is to propose a completely new notion of complexity of logics in finite-model theory. It is the Kolmogorov variant of the Vardi'sexpression complexity. We define it by considering the value of the Kolmogorov complexityC(L[]) of the infinite stringL[] of all truth values of sentences ofLin . The higher is this value, the more expressive is the logicLin . If is a class of finite models, then the value ofC(L[]) over all ∈ is a measure of expressive power ofLin . Unboundedness ofC(L[])−C(L′[]) for ∈ implies nonexistence of a recursive interpretation ofLinL′. A version of this statement with complexities modulo oracles implies the nonexistence of any interpretation ofLinL′. Thus the valuesC(L[]) modulo oracles constitute an invariant of the expressive power of logics over finite models, depending on their real (absolute) expressive power, and not on the syntax. We investigate our notion for fragments of the infinitary logic ^ω_∞ω: least fixed point logic (LFP) and partial fixed point logic (PFP). We prove a precise characterization of 0–1 laws for these logics in terms of a certain boundedness condition placed onC(L[]). We get an extension of the notion of a 0–1 law by imposing an upper bound on the value ofC(L[]) growing not too fast with cardinality of , which still implies inexpressibility results similar to those implied by 0–1 laws. We also discuss classes in whichC(PFP^k[]) is very high. It appears that then PFP or its simple extension can define all the PSPACE subsets of .     

Complexity of Fixed-Size Bit-Vector Logics

Bit-precise reasoning is important for many practical applications of Satisfiability Modulo Theories (SMT). In recent years, efficient approaches for solving fixed-size bit-vector formulas have been developed. From the theoretical point of view, only few results on the complexity of fixed-size bit-vector logics have been published. Some of these results only hold if unary encoding on the bit-width of bit-vectors is used. In our previous work (Kovásznai et al. 2012), we have already shown that binary encoding adds more expressiveness to various fixed-size bit-vector logics with and without quantification. In a follow-up work (Fröhlich et al. 2013), we then gave additional complexity results for several fragments of the quantifier-free case. In this paper, we revisit our complexity results from (Fröhlich et al. 2013; Kovásznai et al. 2012) and go into more detail when specifying the underlying logics and presenting the proofs. We give a better insight in where the additional expressiveness of binary encoding comes from. In order to do this, we bring together our previous work and propose several new complexity results for new fragments and extensions of earlier bit-vector logics. We also discuss the expressiveness of various bit-vector operations in more detail. Altogether, we provide the currently most complete overview on the complexity of common bit-vector logics.     

On the Computational Complexity of Some Classical Equivalence Relations on Boolean Functions

The paper analyzes in terms of polynomial time many-one reductions the computational complexity of several natural equivalence relations on Boolean functions which derive from replacing variables by expressions, one of them is the Boolean isomorphism relation. Most of these computational problems turn out to be between co-NP and ^p ₂ . Received July 1996, and in final form March 1998.     

Hybrid Counterfactual Logics

The purpose of this paper is to argue that the hybrid formalism fits naturally in the context of David Lewis’s counterfactual logic and that its introduction into this framework is desirable. This hybridization enables us to regard the inference “The pig is Mary; Mary is pregnant; therefore the pig is pregnant” as a process of updating local information (which depends on the given situation) by using global information (independent of the situation). Our hybridization also has the following technical advantages: (i) it preserves the completeness and decidability of Lewis’s logic; (ii) it allows us to characterize the Limit Assumption as a proof-rule with some side-conditions; and (iii) it enables us to establish a general Kripke completeness result by using the proof-rule corresponding to the Limit Assumption.     

Hybrid Logics of Separation Axioms

We study hybrid logics in topological semantics. We prove that hybrid logics of separation axioms are complete with respect to certain classes of finite topological models. This characterisation allows us to obtain several further results. We prove that aforementioned logics are decidable and PSPACE-complete, the logics of T ₁ and T ₂ coincide, the logic of T ₁ is complete with respect to two concrete structures: the Cantor space and the rational numbers.     

Undecidability of Multi-modal Hybrid Logics

This paper establishes undecidability of satisfiability for multi-modal logic equipped with the hybrid binder ↓, with respect to frame classes over which the same language with only one modality is decidable. This is in contrast to the usual behaviour of many modal and hybrid logics, whose uni-modal and multi-modal versions do not differ in terms of decidability and, quite often, complexity. The results from this paper apply to a wide range of frame classes including temporally and epistemically relevant ones.     

Display Calculi for Logics with Relative Accessibility Relations

We define cut-free display calculi for knowledge logics wherean indiscernibility relation is associated to each set of agents, andwhere agents decide the membership of objects using thisindiscernibility relation. To do so, we first translate the knowledgelogics into polymodal logics axiomatised by primitive axioms and thenuse Kracht's results on properly displayable logics to define thedisplay calculi. Apart from these technical results, we argue thatDisplay Logic is a natural framework to define cut-free calculi for manyother logics with relative accessibility relations.     

Resolution with Order and Selection for Hybrid Logics

We investigate labeled resolution calculi for hybrid logics with inference rules restricted via selection functions and orders. We start by providing a sound and refutationally complete calculus for the hybrid logic H(@,ˉ,A)\mathcal{H}(@,{\downarrow},\mathsf{A}), even under restrictions by selection functions and orders. Then, by imposing further restrictions in the original calculus, we develop a sound, complete and terminating calculus for the H(@)\mathcal{H}(@) sublanguage. The proof scheme we use to show refutational completeness of these calculi is an adaptation of a standard completeness proof for saturation-based calculi for first-order logic that guarantees completeness even under redundancy elimination. In fact, one of the contributions of this article is to show that the general framework of saturation-based proving for first-order logic with equality can be naturally adapted to saturation-based calculi for other languages, in particular modal and hybrid logics.     

Relations between Average-Case and Worst-Case Complexity

The consequences of the worst-case assumption NP=P are very well understood. On the other hand, we only know a few consequences of the analogous average-case assumption “NP is easy on average.” In this paper we establish several new results on the worst-case complexity of Arthur-Merlin games (the class AM) under the average-case complexity assumption “NP is easy on average.”

Rewriting with Equivalence Relations in ACL2

Traditionally, a conditional rewrite rule directs replacement of one term by another term that is provably equal to it, perhaps under some hypotheses. This paper generalizes the notion of rewrite rule to permit the connecting relation to be merely an equivalence relation. We then extend the algorithm for applying rewrite rules. Applications of these generalized rewrite rules are only admissible in certain equivalential contexts, so the algorithm tracks which equivalence relations are to be preserved and admissible generalized rewrite rules are selected according to this context. We introduce the notions of congruence rule and refinement rule. We also introduce the idea of generated equivalences, corresponding to a new equivalence relation generated by a set of pre-existing ones. Generated equivalences are used to give the rewriter broad access to admissible generalized rewrite rules. We discuss the implementation of these notions in the ACL2 theorem prover. However, the discussion does not assume familiarity with ACL2, and these ideas can be applied to other reasoning systems as well.