Graph decompositions definable in monadic second-order logic

We prove that the split decomposition of a graph is definable by Monadic Second-Order formulas. We also prove that the set of graphs having the same cycle matroid as a given graph is definable from this graph by Monadic Second-Order formulas. These results are consequences of general results on the logical definability of graph decompositions of various types.     

On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic

We discuss the parametrized complexity of counting and evaluation problems on graphs where the range of counting is definable in monadic second-order logic (MSOL). We show that for bounded tree-width these problems are solvable in polynomial time. The same holds for bounded clique width in the cases, where the decomposition, which establishes the bound on the clique-width, can be computed in polynomial time and for problems expressible by monadic second-order formulas without edge set quantification. Such quantifications are allowed in the case of graphs with bounded tree-width. As applications we discuss in detail how this affects the parametrized complexity of the permanent and the hamiltonian of a matrix, and more generally, various generating functions of MSOL definable graph properties. Finally, our results are also applicable to SAT and ♯SAT.     

On arithmetical completeness of the logic of proofs

In this paper, we establish a stronger version of Artemov's arithmetical completeness theorem of the Logic of Proofs ${\mathsf{LP}}_0$. Moreover, we prove a version of the uniform arithmetical completeness theorem of ${\mathsf{LP}}_0$.     

On the polynomial-space completeness of intuitionistic propositional logic

We present an alternative, purely semantical and relatively simple, proof of the Statman's result that both intuitionistic propositional logic and its implicational fragment are PSPACE-complete.This paper was supported by grant 401/01/0218 of the Grant Agency of the Czech Republic. % Mathematics Subject Classification (2000):     

Provability logic and the completeness principle

The logic $\mathsf{iGLC}$ is the intuitionistic version of Löb's Logic plus the completeness principle $A\to \square A$. In this paper, we prove an arithmetical completeness theorems for $\mathsf{iGLC}$ for theories equipped with two provability predicates □ and △ that prove the schemes $A\to △A$ and $\square △S\to \square S$ for $S\in {\mathrm{\Sigma }}_1$. We provide two salient instances of the theorem. In the first, □ is fast provability and △ is ordinary provability and, in the second, □ is ordinary provability and △ is slow provability.Using the second instance, we reprove a theorem previously obtained by Mohammad Ardeshir and Mojtaba Mojtahedi [1] determining the ${\mathrm{\Sigma }}_1$-provability logic of Heyting Arithmetic.     

Intuitionistic completeness of first-order logic

We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.     

Strong completeness of lattice-valued logic

 Strong completeness of S. Titani's system for lattice valued logic is shown by means of Dedekind cuts. Received: 26 June 2000 / Published online: 31 May 2002     

Topological completeness of the provability logic GLP

Provability logic GLP is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces are called GLP-spaces whenever they satisfy all the axioms of GLP. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces.     

A note on decidability of variables in intuitionistic propositional logic

An answer to the following question is presented: given a proof in classical propositional logic, for what small set of propositional variables p does it suffice to add all the formulae to Γ in order to intuitionistically prove A? This answer is an improvement of Ishihara's result for some cases.     

Pavelka-style completeness in expansions of Łukasiewicz logic

An algebraic setting for the validity of Pavelka style completeness for some natural expansions of Łukasiewicz logic by new connectives and rational constants is given. This algebraic approach is based on the fact that the standard MV-algebra on the real segment [0, 1] is an injective MV-algebra. In particular the logics associated with MV-algebras with product and with divisible MV-algebras are considered. The author express his gratitude to Roberto Cignoli, for his advice during the preparation of this paper.     

On the expressiveness and decidability of o-minimal hybrid systems

This paper is driven by a general motto: bisimulate a hybrid system by a finite symbolic dynamical system. In the case of o-minimal hybrid systems, the continuous and discrete components can be decoupled, and hence, the problem reduces in building a finite symbolic dynamical system for the continuous dynamics of each location. We show that this can be done for a quite general class of hybrid systems defined on o-minimal structures. In particular, we recover the main result of a paper by G. Lafferriere, G.J. Pappas, and S. Sastry, on o-minimal hybrid systems. We also provide an analysis and extension of results on decidability and complexity of problems and constructions related to o-minimal hybrid systems.     

Notes on monadic logic. part A. Monadic theory of the real line

The second-order theory of the continuum in the Cohen extension of a set-theoretic universe is interpreted in the monadic theory of the real line and may be interpreted in the monadic topology of Cantor’s discontinuum as well.     

A sequent calculus for logic of knowledge and past time: Completeness and decidability

We consider logic of knowledge and past time. This logic involves the discrete-time linear temporal operators next, until, weak yesterday, and since. In addition, it contains an indexed set of unary modal operators agent i knows.We consider the semantic constraint of the unique initial states for this logic. For the logic, we present a sequent calculus with a restricted cut rule. We prove the soundness and completeness of the sequent calculus presented. We prove the decidability of provability in the considered calculus as well. So, this calculus can be used as a basis for automated theorem proving. The proof method for the completeness can be used to construct complete sequent calculi with a restricted cut rule for this logic with other semantical constraints as well. Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 3, pp. 427–437, July–September, 2006.