On the number of variables in undecidable superintuitionistic propositional calculi [PDF]
18 pages, 1 ...
Grigoriy V. Bokov
openalex +4 more sources
Propositional Independence - Formula-Variable Independence and Forgetting
Independence -- the study of what is relevant to a given problem of reasoning -- has received an increasing attention from the AI community. In this paper, we consider two basic forms of independence, namely, a syntactic one and a semantic one. We show features and drawbacks of them.
J. Lang +2 more
openalex +8 more sources
Classical propositional logic and decidability of variables in intuitionistic propositional logic [PDF]
We improve the answer to the question: what set of excluded middles for propositional variables in a formula suffices to prove the formula in intuitionistic propositional logic whenever it is provable in classical propositional logic.
Hajime Ishihara
openalex +7 more sources
Complexity and expressivity of propositional dynamic logics with finitely many variables [PDF]
We investigate the complexity of satisfiability for finite-variable fragments of propositional dynamic logics. We consider three formalisms belonging to three representative complexity classes, broadly understood,---regular PDL, which is EXPTIME-complete, PDL with intersection, which is 2EXPTIME-complete, and PDL with parallel composition, which is ...
Mikhail Rybakov, Dmitry Shkatov
openalex +5 more sources
Individual concepts as propositional variables in ${\rm ML}^{\nu+1}$. [PDF]
The author studies the many-sorted quantified modal systems defined previously by \textit{A. Bressan} [A general interpreted modal calculus (1972; Zbl 0255.02015); Aspects of philosophical logic, Synth. Libr. 147, 21-66 (1981; Zbl 0476.03028)]. \(ML^{\nu}\) (\(\nu\) : a positive integer) is a typed language, \(MC^{\nu}\) is a calculus (an extension of ...
Alberto Zanardo
openalex +5 more sources
Monodic temporal logic with quantified propositional variables [PDF]
We extend the monodic fragment of first-order linear temporal logic to include right-linear grammar operators and quantification of propositional variables. Unlike propositional temporal logic, the use of grammar operators in first-order temporal logic is not equivalent to general propositional quantification, as the latter admit satisfiable formulae ...
Walter Hussak
openalex +3 more sources
On the proposition $C\delta CpqC\delta p\delta q$ with a variable functor [PDF]
Summary: In this note, we shall prove that \(CcCpqCpcq\) implies 1) \(CpCqp\), 2) \(CCpCqrCCpqCpr\), 3) \(CCCpqpp\).
Shôtarô Tanaka
openalex +3 more sources
The model checking problem for intuitionistic propositional logic with one variable is AC1-complete [PDF]
We show that the model checking problem for intuitionistic propositional logic with one variable is complete for logspace-uniform AC1. As basic tool we use the connection between intuitionistic logic and Heyting algebra, and investigate its complexity ...
Mundhenk, Martin, Weiss, Felix
core +3 more sources
The decidability of one-variable propositional calculi. [PDF]
M. D. Gladstone
openalex +5 more sources
On complexity of propositional linear-time temporal logic with finitely many variables [PDF]
It is known [DemriSchnoebelen02] that both satisfiability and model-checking problems for propositional Linear-time Temporal Logic, LTL, with only a single propositional variable in the language are PSPACE-complete, which coincides with the complexity of these problems for LTL with an arbitrary number of propositional variables [SislaClarke85].
Mikhail Rybakov, Dmitry Shkatov
openalex +6 more sources

