素数阶群理论的量词消去算法及其上界

在以前的一些工作中,作者已经证明语言(?)={+,0,e)上素数阶群的理论T有量词消去性质并研究了它的判定问题的复杂性.本文在此基础上将利用T的判定问题的复杂性结果给出理论T的量词消去的一个算法,同时给出该算法的复杂性上界.     

可量词消去的带根节点的树理论

讨论了带根节点r的有向树、无向树理论的量词消去性质,找到决定理论量词消去的三类特殊公式,并给出了在语言■_0={E,r}(E为有向边或无向边)及添加二元距离关系D_(n,n)w所得膨胀语言下,可量词消去的这两类理论的完全分类.     

可量词消去的树形偏序理论的分类

提出了偏序的全序片段、序模式的概念以刻画树形偏序的结构特征,以此为基础,讨论了有最小元0的树形偏序理论的量词消去性质,给出了在语言(?)_0={,0}及其膨胀语言下可以量词消去的这类理论的完全分类。     

完全二叉树的量词消去

量词消去法已经成为计算机科学和代数模型论中最有力的研究工具之一.本 文针对完全二叉树理论所独有的特性,给出了它的基本公式集,然后利用分布公式及 有限覆盖证明了完全二叉树的理论可以量词消去.     

完全二叉树理论的计算复杂度

完全二叉树的一阶理论已被证明具有量词消去的性质,进而计算了完全二叉树模型中元素的CB秩.本文利用有界Ehrenfeucht-Frassé博弈研究完全二叉树的一阶理论,证明了此理论的时间计算复杂度上界为22cn,空间计算复杂度上界为2dn(其中n为输入长度,c,d为合适的常数).     

完全二叉树模型中元素的CB秩

本文以完全二叉树理论的可量词消去为基础,介绍了该理论的可数原子模型 及饱和模型,并计算了一元、二元完全型的CB秩,从而给出了CB秩在该理论中的 几何解释.     

完全二叉树模型中元素的CB秩

本文以完全二叉树理论的可量词消去为基础,介绍了该理论的可数原子模型 及饱和模型,并计算了一元、二元完全型的CB秩,从而给出了CB秩在该理论中的 几何解释.     

非线性Lipschitz算子的定量性质(V)──数值值域

本文引入 Ｂａｎａｃｈ空间上非线性 Ｌｉｐｓｃｈｉｔｚ算子 Ｔ的另一个重要定量特性——数值值域Ｗ（Ｔ）．我们证明： Ｗ（Ｔ）与Ｇｅｒｓｃｈｇｏｉｎ域Ｇ（Ｔ）及谱集σ（Ｔ）具有关系σ（Ｔ） ■ ＣｏＷ（Ｔ）＝ Ｇ（Ｔ）．同时,利用此数值域,我们对算子可逆,稳定与压缩的定量性质进行了深入的研究．     

枢轴消去变换的若干性质

得到了与Gauss消去变换有着密切联系的枢轴消去变换的三个重要性质.     

可除剩余格中的消去律

首先,通过对可除剩余格性质的进一步探究,给出了可除剩余格中的蕴涵左消去律;其次,结合剩余格中"′"运算的性质,证明了正则条件下的蕴涵右消去律的存在性;最后,根据""和"→"的伴随性质,进一步探讨了正则可除剩余格中的乘法消去律的表现形式。     

The logic of integration

We develop a model theoretic framework for studying algebraic structures equipped with a measure. The real line is used as a value space and its usual arithmetical operations as connectives. Integration is used as a quantifier. We extend some basic results of pure model theory to this context and characterize measurable sets in terms of zero-sets of formulas.      

Monadic dynamic algebras

The main purpose of this work is to introduce the class of the monadic dynamic algebras (dynamic algebras with one quantifier). Similarly to a theorem of Kozen we establish that every separable monadic dynamic algebra is isomorphic to a monadic (possibly non‐standard) Kripke structure. We also classify the simple (monadic) dynamic algebras. Moreover, in the dynamic duality theory, we analyze the conditions under which a hemimorphism of a dynamic algebra into itself defines a quantifier. (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Completeness and interpolation of almost‐everywhere quantification over finitely additive measures

We give an axiomatization of first‐order logic enriched with the almost‐everywhere quantifier over finitely additive measures. Using an adapted version of the consistency property adequate for dealing with this generalized quantifier, we show that such a logic is both strongly complete and enjoys Craig interpolation, relying on a (countable) model existence theorem. We also discuss possible extensions of these results to the almost‐everywhere quantifier over countably additive measures.     

Hilbert spaces expanded with a unitary operator

We study Hilbert spaces expanded with a unitary operator with a countable spectrum. We show that the theory of such a structure is ω ‐stable and admits quantifier elimination. (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Quantifier elimination for the theory of algebraically closed valued fields with analytic structure

The theory of algebraically closed non‐Archimedean valued fields is proved to eliminate quantifiers in an analytic language similar to the one used by Cluckers, Lipshitz, and Robinson. The proof makes use of a uniform parameterized normalization theorem which is also proved in this paper. This theorem also has other consequences in the geometry of definable sets. The method of proving quantifier elimination in this paper for an analytic language does not require the algebraic quantifier elimination theorem of Weispfenning, unlike the customary method of proof used in similar earlier analytic quantifier elimination theorems. (© 2007 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

An Intuitionistic Axiomatisation of Real Closed Fields

We give an intuitionistic axiomatisation of real closed fields which has the constructive reals as a model. The main result is that this axiomatisation together with just the decidability of the order relation gives the classical theory of real closed fields. To establish this we rely on the quantifier elimination theorem for real closed fields due to Tarski, and a conservation theorem of classical logic over intuitionistic logic for geometric theories.