Modal Logics of Stone Spaces

Interpreting modal diamond as the closure of a topological space, we axiomatize the modal logic of each metrizable Stone space and of each extremally disconnected Stone space. As a corollary, we obtain that S4.1 is the modal logic of the Pelczynski compactification of the natural numbers and S4.2 is the modal logic of the Gleason cover of the Cantor space. As another corollary, we obtain an axiomatization of the intermediate logic of each metrizable Stone space and of each extremally disconnected Stone space. In particular, we obtain that the intuitionistic logic is the logic of the Pelczynski compactification of the natural numbers and the logic of weak excluded middle is the logic of the Gleason cover of the Cantor space.     

Barwise's Information Frames and Modal Logics

The article studies Barwise's information frames and settles the problem of Barwise dealing in finding axiomatizations for the modal logics generated by information frames. We find axiomatic systems for: (i) the modal logic of all complete information frames; (ii) the logic of all sound and complete information frames; (iii) the logic of all hereditary and complete information frames; (iv) the logic of all complete, sound, and hereditary information frames; (v) the logic of all consistent and complete information frames. The notion of weak modal logics is also proposed, and it is shown that the weak modal logics generated by all information frames and by all hereditary information frames are K and K4, respectively. Toward a general theory, we prove that any Kripke complete modal logic is a modal logic of a certain class of information frames, and that every modal logic generated by any given class of complete, rarefied, and fully classified information frames is Kripke complete.     

The Frobenius Problem for Classes of Polynomial Solvability

The Frobenius problem is to find a method ( $ =$ algorithm) for calculating the largest “sum of money” that cannot be given by coins whose values $b_0 ,{\text{ }}b_1 ,{\text{ }} \ldots {\text{, }}b_w$ are coprime integers. As admissible solutions (algorithms), it is common practice to study polynomial algorithms, which owe their name to the form of the dependence of time expenditure on the length of the original information. The difficulty of the Frobenius problem is apparent from the fact that already for $w = 3$ the existence of a polynomial solution is still an open problem. In the present paper, we distinguish some classes of input data for which the problem can be solved polynomially; nevertheless, argumentation in the spirit of complexity theory of algorithms is kept to a minimum.     

Polynomial Computability of Certain Rudimentary Predicates

The class of rudimentary predicates is defined as the smallest class of numerical predicates that contains the equality and concatenation predicates and is closed under the operations of propositional logic, explicit transformations, and bounded quantification. Two classes of rudimentary predicates are considered. The first of them consists of the predicates whose prenex normal form of a special type has the quantifier prefix of the form . Predicates of the second class can have an arbitrary quantifier prefix, but restrictions are imposed on the Skolem deciding functions. It is proved that any predicate from each of these classes can be computed by a suitable deterministic algorithm in polynomial time.     

Modal Extensions of Sub-classical Logics for Recovering Classical Logic

In this paper we introduce non-normal modal extensions of the sub-classical logics CLoN, CluN and CLaN, in the same way that S0.5 ⁰ extends classical logic. The first modal system is both paraconsistent and paracomplete, while the second one is paraconsistent and the third is paracomplete. Despite being non-normal, these systems are sound and complete for a suitable Kripke semantics. We also show that these systems are appropriate for interpreting □ as “is provable in classical logic”. This allows us to recover the theorems of propositional classical logic within three sub-classical modal systems.     

Application of Modal Logics to the Specification and Verification of Programs

Temporal logic methods and algorithms are used for verifying programs. A method employing temporal semantic tables is proposed for studying the properties of dynamic processes.     

完全域上矩阵多项式方程的可解性

本文利用一般域上的λ-矩阵理论，研究了矩阵多项式方程的可解性，证明了完全域上矩阵多项式方程有解的充要条件，这些条件同时提供了解此类矩阵方程的方法。     

Hilbert Polynomial of a Certain Ladder-Determinantal Ideal

A ladder-shaped array is a subset of a rectangular array which looks like a Ferrers diagram corresponding to a partition of a positive integer. The ideals generated by the p-by-p minors of a ladder-type array of indeterminates in the corresponding polynomial ring have been shown to be hilbertian (i.e., their Hilbert functions coincide with Hilbert polynomials for all nonnegative integers) by Abhyankar and Kulkarni [3, p 53–76]. We exhibit here an explicit expression for the Hilbert polynomial of the ideal generated by the two-by-two minors of a ladder-type array of indeterminates in the corresponding polynomial ring. Counting the number of paths in the corresponding rectangular array having a fixed number of turning points above the path corresponding to the ladder is an essential ingredient of the combinatorial construction of the Hilbert polynomial. This gives a constructive proof of the hilbertianness of the ideal generated by the two-by-two minors of a ladder-type array of indeterminates.     

Unique Solvability of Certain Hybrid Networks from Their Distances

Phylogenetic relationships among taxa have usually been represented by rooted trees in which the leaves correspond to extant taxa and interior vertices correspond to extinct ancestral taxa. Recently, more general graphs than trees have been investigated in order to be able to represent hybridization, lateral gene transfer, and recombination events. A model is presented in which the genome at a vertex is represented by a binary string. In the presence of hybridization and the absence of convergent evolution and homoplasies, the evolution is modeled by an acyclic digraph. It is shown how distances are most naturally related to the vertices rather than to the edges. Indeed, distances are computed in terms of the “originating weights” at vertices. It is shown that some distances may not in fact correspond to the sum of branch lengths on any path in the graph. In typical applications, direct measurements can be made only on the leaves, including the root. A study is made of how to infer the originating weights at interior vertices from such information. Received August 18, 2004     

一类Toeplitz线性方程组与多项式除法的复杂性

本文给出带状Toeplitz线性方程组,带状三角Toeplitz线性方程组求解的快速方法,其方法基于三角Toeplitz方程与Toeplitz方程的快速求解.并由此给出了一般多次式除法的新算法.     

On the Mosaic Method for Many-Dimensional Modal Logics: A Case Study Combining Tense and Modal Operators

We present an extension of the mosaic method aimed at capturing many-dimensional modal logics. As a proof-of-concept, we define the method for logics arising from the combination of linear tense operators with an “orthogonal” S5-like modality. We show that the existence of a model for a given set of formulas is equivalent to the existence of a suitable set of partial models, called mosaics, and apply the technique not only in obtaining a proof of decidability and a proof of completeness for the corresponding Hilbert-style axiomatization, but also in the development of a mosaic-based tableau system. We further consider extensions for dealing with the case when interactions between the two dimensions exist, thus covering a wide class of bundled Ockhamist branching-time logics, and present for them some partial results, such as a non-analytic version of the tableau system.     

On the Finite Model Property of Intuitionistic Modal Logics over MIPC

MIPC is a well-known intuitionistic modal logic of Prior (1957) and Bull (1966). It is shown that every normal intuitionistic modal logic L over MIPC has the finite model property whenever L is Kripke-complete and universal.