相关论文: Automated reasoning for proving non-orderability o…

The notion of clause set cycle abstracts a family of methods for automated inductive theorem proving based on the detection of cyclic dependencies between clause sets. By discerning the underlying logical features of clause set cycles, we…

We identify a number of decidable and undecidable fragments of first-order concatenation theory. We also give a purely universal axiomatization which is complete for the fragments we identify. Furthermore, we prove some normal-form results.

I investigate modal group theory for arbitrary homomorphisms. Possibility is interpreted by the existence of a group homomorphism out of the given group, so the semantics is governed by the possibility of collapse: elements may be…

In this paper we begin the systematic study of group equations with abelian predicates in the main classes of groups where solving equations is possible. We extend the line of work on word equations with length constraints, and more…

We formulate and discuss a general axiomatic theory of arbitrary objects. This theory is expressed in a simple first-order language without modal operators, and it is governed by classical logic.

Let $X$ be any scheme defined over a Dedekind scheme $S$ with a given section $x\in X(S)$. We prove the existence of a pro-finite $S$-group scheme $\aleph(X,x)$ and a universal $\aleph(X,x)$-torsor dominating all the pro-finite pointed…

We prove the orderability of the Witzel-Zaremsky-Thompson group for a direct system of orderable groups under a certain compatibility assumption.

We prove that the word problem for the infinite cyclic group is not EDT0L, and obtain as a corollary that a finitely generated group with EDT0L word problem must be torsion. In addition, we show that the property of having an EDT0L word…

We describe a method for proving non-looping non-termination, that is, of term rewriting systems that do not admit looping reductions. As certificates of non-termination, we employ regular (tree) automata.

We prove a new criterion for the solvability of the finite groups, depending on the function $\psi_k(G)$ which is defined as the sum of $k$-th powers of the element orders of $G$. We show that our result can be used to show the solvability…

We construct a finitely presented (two-sided) totally orderable group with insoluble word problem.

We prove Roth type theorems in finite groups. Our main tool is the Triangle Removal Lemma of Ruzsa and Szemer\'edi.

For any first order theory T we construct a Boolean valued model M, in which precisely the T--provable formulas hold, and in which every (Boolean valued) subset which is invariant under all automorphisms of M is definable by a first order…

In this paper we develop cyclic proof systems for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the inductive definitions belong to the quantifier-free fragments…

This is a draft of a book submitted for publication by the AMS. Its theme is the remarkable interplay, accelerating in the last few decades, between topology and the theory of orderable groups, with applications in both directions. It…

Models of a generalized nondeterminism are defined by limitations on nonde- terministic behavior of a computing device. A regular realizability problem is a problem of verifying existence of a special sort word in a regular language. These…

In this paper we give an ordinal analysis of the theory of second order arithmetic. We do this by working with proof trees -- that is, "deductions" which may not be well-founded. Working in a suitable theory, we are able to represent…

In this paper we give a polynomial-time quantum algorithm for computing orders of solvable groups. Several other problems, such as testing membership in solvable groups, testing equality of subgroups in a given solvable group, and testing…

We lay down the fundations of the theory of groups of finite Morley rank in which local subgroups are solvable and we proceed to the local analysis of these groups. We prove the main Uniqueness Theorem, analogous to the Bender method in…

Accretive and monotone operator theory are central branches of nonlinear functional analysis and constitute the abstract study of set-valued mappings between function spaces. This paper deals with the computational properties of certain…