No Arabic abstract
We are interested in solving decision problem $exists? t in mathbb{N}, cos t theta = c$ where $cos theta$ and $c$ are algebraic numbers. We call this the $cos t theta$ problem. This is an exploration of Diophantine equations with analytic functions. Polynomial, exponential with real base and cosine function are closely related to this decision problem: $ exists ? t in mathbb{N}, u^T M^t v = 0$ where $u, v in mathbb{Q}^n, M in mathbb{Q}^{ntimes n}$. This problem is also known as Skolem problem and is useful in verification of linear systems. Its decidability remains unknown. Single variable Diophantine equations with exponential function with real algebraic base and $cos t theta$ function with $theta$ a rational multiple of $pi$ is decidable. This idea is central in proving the decidability of Skolem problem when the eigenvalues of $M$ are roots of real numbers. The main difficulty with the cases when eigenvalues are not roots of reals is that even for small order cases decidability requires application of trancendental number theory which does not scale for higher order cases. We provide a first attempt to overcome that by providing a $PTIME$ algorithm for $cos t theta$ when $theta$ is not a rational multiple of $pi$. We do so without using techniques from transcendental number theory. par One of the main difficulty in Diophantine equations is being unable to use tools from calculus to solve this equation as the domain of variable is $mathbb{N}$. We also provide an attempt to overcome that by providing reduction of Skolem problem to solving a one variable equation (which involves polynomials, exponentials with real bases and $cos t theta$ function with $t$ ranging over reals and $theta in [0, pi]$) over reals.
In the present paper we show that there are infinitely many classes of term functions in the free-void generated diagonalizable algebra, which are precomplete with respect to parametrical expressibility of functions.
For formulas F of propositional calculus I introduce a metavariable MF and show how it can be used to define an algorithm for testing satisfiability. MF is a formula which is true/false under all possible truth assignments iff F is satisfiable/unsatisfiable. In this sense MF is a metavariable with the meaning F is SAT. For constructing MF a group of transformations of the basic variables ai is used which corresponds to flipping literals to their negation. The whole procedure corresponds to branching algorithms where a formula is split with respect to the truth values of its variables, one by one. Each branching step corresponds to an approximation to the metatheorem which doubles the chance to find a satisfying truth assignment but also doubles the length of the formulas to be tested, in principle. Simplifications arise by additional length reductions. I also discuss the notion of logical primes and show that each formula can be written as a uniquely defined product of such prime factors. Satisfying truth assignments can be found by determining the missing primes in the factorization of a formula.
In this paper, first-order logic is interpreted in the framework of universal algebra, using the clone theory developed in three previous papers. We first define the free clone T(L, C) of terms of a first order language L over a set C of parameters in a standard way. The free right algebra F(L, C) of formulas over T(L, C) is then generated by atomic formulas. Structures for L over C are represented as perfect valuations of F(L, C), and theories of L are represented as filters of F(L). Finally Godels completeness theorem and first incompleteness theorem are stated as expected.
The development of compositional distributional models of semantics reconciling the empirical aspects of distributional semantics with the compositional aspects of formal semantics is a popular topic in the contemporary literature. This paper seeks to bring this reconciliation one step further by showing how the mathematical constructs commonly used in compositional distributional models, such as tensors and matrices, can be used to simulate different aspects of predicate logic. This paper discusses how the canonical isomorphism between tensors and multilinear maps can be exploited to simulate a full-blown quantifier-free predicate calculus using tensors. It provides tensor interpretations of the set of logical connectives required to model propositional calculi. It suggests a variant of these tensor calculi capable of modelling quantifiers, using few non-linear operations. It finally discusses the relation between these variants, and how this relation should constitute the subject of future work.
This note introduces a generalization to the setting of infinite-time computation of the busy beaver problem from classical computability theory, and proves some results concerning the growth rate of an associated function. In our view, these results indicate that the generalization is both natural and promising.