Computational complexity of hybrid interval temporal logics

Interval logics are very expressive temporal formalisms, but reasoning with them is often undecidable or has high computational complexity. As a result, a vast number of approaches limiting their expressive power—in order to obtain better computational behaviour—have been introduced. Unfortunately, due to such restrictions, interval logics often lose referentiality, that is, the capacity to refer to specific time intervals, which is crucial for temporal representation and reasoning. The computational price that needs to be paid in order to regain referentiality is not well studied and our research aims to fill this gap. In particular we study the main interval temporal logic, called the Halpern-Shoham logic, and its low complexity modifications. To regain referentiality in these modifications, we extend the language with the hybrid machinery—nominals and satisfaction operators—and classify the obtained logics according to their computational complexity. We show that such a hybridisation often makes tractable logics intractable but not undecidable. This allows us to construct hybrid interval temporal logics which are referential as well as maintain a good compromise between expressiveness and complexity; it makes them valuable formalisms for temporal knowledge representation. We also introduce a class of models which, due to a specific interplay between the interpretation of modal operators and a structure of time, makes reasoning in interval logics computationally hard even in the absence of the hybrid machinery.     

The polynomial bounds of proof complexity in Frege systems

The concept of a determinative set of variables for a propositional formula was introduced by one of the authors, which made it possible to distinguish the set of hard-determinable formulas. The proof complexity of a formula of this sort has exponential lower bounds in some proof systems of classical propositional calculus (cut-free sequent system, resolution system, analytic tableaux, cutting planes, and bounded Frege systems). In this paper we prove that the property of hard-determinability is insufficient for obtaining a superpolynomial lower bound of proof lines (sizes) in Frege systems: an example of a sequence of hard-determinable formulas is given whose proof complexities are polynomially bounded in every Frege system.     

An approach to infinitary temporal proof theory

Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an –type schema of inference that naturally interpret the propositional and the predicate until–free fragments of Linear Time Logic LTL respectively. The two calculi are based on a natural extension of ordinary sequents and of standard modal rules. We examine the pure propositional case (no extralogical axioms), the propositional and the first order predicate cases (both with a possibly infinite set of extralogical axioms). For each system we provide a syntactic proof of cut elimination and a proof of completeness.Supported by MIUR COFIN 02 Teoria dei Modelli e Teoria degli Insiemi, loro interazioni ed applicazioni.Supported by MIUR COFIN 02 PROTOCOLLO.Mathematics Subject Classification (2000):03B22, 03B45, 03F05     

On unification and admissible rules in Gabbay–de Jongh logics

In this paper we study the admissible rules of intermediate logics. We establish some general results on extensions of models and sets of formulas. These general results are then employed to provide a basis for the admissible rules of the Gabbay–de Jongh logics and to show that these logics have finitary unification type.     

The proof theoretic strength of the Steinitz exchange theorem

We show that the logical theory QLA proves the Cayley-Hamilton theorem from the Steinitz exchange theorem together with a strengthening of the linear independence principle. Since QLA is a fairly weak theory (in the sense that its quantifier-free fragment, LA, translates into tautologies with TC⁰-Frege proofs—when restricted to the field Q of the rationals), it follows that the proof complexity of matrix algebra can be distilled to the Steinitz exchange theorem.     

Prefinitely axiomatizable modal and intermediate logics

A logic Λ bounds a property P if all proper extensions of Λ have P while Λ itself does not. We construct logics bounding finite axiomatizability and logics bounding finite model property in the lattice of intermediate logics and in the lattice of normal extensions of K4.3. MSC: 03B45, 03B55.     

Proof complexity of intuitionistic implicational formulas

We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions.In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrube? (2007), generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Je?ábek (2009), can be realized by implicational tautologies.     

Monotone Proofs of the Pigeon Hole Principle

We study the complexity of proving the Pigeon Hole Principle (PHP)in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We prove a size‐depth trade‐off upper bound for monotone proofs of the standard encoding of the PHP as a monotone sequent. At one extreme of the trade‐off we get quasipolynomia ‐size monotone proofs, and at the other extreme we get subexponential‐size bounded‐depth monotone proofs. This result is a consequence of deriving the basic properties of certain monotone formulas computing the Boolean threshold functions. We also consider the monotone sequent expressing the Clique‐Coclique Principle (CLIQUE) defined by Bonet, Pitassi and Raz [9]. We show that monotone proofs for this sequent can be easily reduced to monotone proofs of the one‐to‐one and onto PHP, and so CLIQUE also has quasipolynomia ‐size monotone proofs. As a consequence of our results, Resolution, Cutting Planes with polynomially bounded coefficients, and Bounded‐Depth Frege are exponentially separated from the monotone Gentzen Calculus. Finally, a simple simulation argument implies that these results extend to the Intuitionistic Gentzen Calculus. Our results partially answer some questions left open by P. Pudlák.     

Reasoning about proof and knowledge

In previous work [15], we presented a hierarchy of classical modal systems, along with algebraic semantics, for the reasoning about intuitionistic truth, belief and knowledge. Deviating from Gödel's interpretation of IPC in S4, our modal systems contain IPC in the way established in [13]. The modal operator can be viewed as a predicate for intuitionistic truth, i.e. proof. Epistemic principles are partially adopted from Intuitionistic Epistemic Logic IEL [4]. In the present paper, we show that the S5-style systems of our hierarchy correspond to an extended Brouwer–Heyting–Kolmogorov interpretation and are complete w.r.t. a relational semantics based on intuitionistic general frames. In this sense, our S5-style logics are adequate and complete systems for the reasoning about proof combined with belief or knowledge. The proposed relational semantics is a uniform framework in which also IEL can be modeled. Verification-based intuitionistic knowledge formalized in IEL turns out to be a special case of the kind of knowledge described by our S5-style systems.     

Axiomatizations of team logics

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-preserving elimination of modalities and quantifiers from formulas.     

The Skolemization of prenex formulas in intermediate logics

The skolem class of a logic consists of the formulas for which the derivability of the formula is equivalent to the derivability of its Skolemization. In contrast to classical logic, the skolem classes of many intermediate logics do not contain all formulas. In this paper it is proven for certain classes of propositional formulas that any instance of them by (independent) predicate sentences in prenex normal form belongs to the skolem class of any intermediate logic complete with respect to a class of well-founded trees. In particular, all prenex sentences belong to the skolem class of these logics, and this result extends to the constant domain versions of these logics.     

Complexity of admissible rules

We investigate the computational complexity of deciding whether a given inference rule is admissible for some modal and superintuitionistic logics. We state a broad condition under which the admissibility problem is coNEXP-hard. We also show that admissibility in several well-known systems (including GL, S4, and IPC) is in coNE, thus obtaining a sharp complexity estimate for admissibility in these systems. The research was done while the author was visiting the Department of Philosophy of the Utrecht University. Supported by grant IAA1019401 of GA AV ČR     

Analyzing completeness of axiomatic functional systems for temporal × modal logics

In previous works, we presented a modification of the usual possible world semantics by introducing an independent temporal structure in each world and using accessibility functions to represent the relation among them. Different properties ofthe accessibility functions (being injective, surjective, increasing, etc.) have been considered and axiomatic systems (called functional) which define these properties have been given. Only a few ofthese systems have been proved tobe complete. The aim ofthis paper is to make a progress in the study ofcompleteness for functional systems. For this end, we use indexes as names for temporal flows and give new proofs of completeness. Specifically, we focus our attention on the system which defines injectivity, because the system which defines this property without using indexes was proved to be incomplete in previous works. The only system considered which remains incomplete is the one which defines surjectivity, even ifwe consider a sequence ofnatural extensions ofthe previous one (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)