Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userCan one design a geometry engine? On the (un)decidability of affine Euclidean geometries
52
0
0.0
(
0
)
Added by
Johann Makowsky
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Authors
J.A. Makowsky
Ask ChatGPT about the research
No Arabic abstract
We survey the status of decidabilty of the consequence relation in various axiomatizations of Euclidean geometry. We draw attention to a widely overlooked result by Martin Ziegler from 1980, which proves Tarskis conjecture on the undecidability of finitely axiomatizable theories of fields. We elaborate on how to use Zieglers theorem to show that the consequence relations for the first order theory of the Hilbert plane and the Euclidean plane are undecidable. As new results we add: (A) The first order consequence relations for Wus orthogonal and metric geometries (Wen-Tsun Wu, 1984), and for the axiomatization of Origami geometry (J. Justin 1986, H. Huzita 1991)are undecidable. It was already known that the universal theory of Hilbert planes and Wus orthogonal geometry is decidable. We show here using elementary model theoretic tools that (B) the universal first order consequences of any geometric theory $T$ of Pappian planes which is consistent with the analytic geometry of the reals is decidable.
rate research
Read More
Let $K$ be a field equipped with a valuation. Tropical varieties over $K$ can be defined with a theory of Gr{o}bner bases taking into account the valuation of $K$.Because of the use of the valuation, the theory of tropical Gr{o}bner bases has proved to provide settings for computations over polynomial rings over a $p$-adic field that are more stable than that of classical Gr{o}bner bases.Beforehand, these strategies were only available for homogeneous polynomials. In this article, we extend the F5 strategy to a new definition of tropical Gr{o}bner bases in an affine setting.We provide numerical examples to illustrate time-complexity and $p$-adic stability of this tropical F5 algorithm.We also illustrate its merits as a first step before an FGLM algorithm to compute (classical) lex bases over $p$-adics.
Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the domain stays the same across worlds, or not. In particular, we show that the bundle $forall Box$ is undecidable over constant domain interpretations, even with only monadic predicates, whereas $exists Box$ bundle is decidable. On the other hand, over increasing domain interpretations, we get decidability with both $forall Box$ and $exists Box$ bundles with unrestricted predicates. In these cases, we also obtain tableau based procedures that run in PSPACE. We further show that the $exists Box$ bundle cannot distinguish between constant domain and increasing domain interpretations.
Four points ordered in the positive order on the unit circle determine the vertices of a quadrilateral, which is considered either as a euclidean or as a hyperbolic quadrilateral depending on whether the lines connecting the vertices are euclidean or hyperbolic lines. In the case of hyperbolic lines, this type of quadrilaterals are called ideal quadrilaterals. Our main result gives a euclidean counterpart of an earlier result on the hyperbolic distances between the opposite sides of ideal quadrilaterals. The proof is based on computations involving hyperbolic geometry. We also found a new formula for the hyperbolic midpoint of a hyperbolic geodesic segment in the unit disk. As an application of some geometric properties, we provided a euclidean construction of the symmetrization of random four points on the unit circle with respect to a diameter which preserves the absolute cross ratio of quadruples.
This paper deals essentially with affine or projective transformations of Lie groups endowed with a flat left invariant affine or projective structure. These groups are called flat affine or flat projective Lie groups. Our main results determine Lie groups admitting flat bi-invariant affine or projective structures. These groups could play an essential role in the study of homogeneous spaces $M=G/H$ admitting flat affine or flat projective structures invariant under the natural action of $G$ on $M$. A. Medina asked several years ago if the group of affine transformations of a flat affine Lie group is a flat projective Lie group. In this work we provide a partial possitive answer to this question.
In an emerging computing paradigm, computational capabilities, from processing power to storage capacities, are offered to users over communication networks as a cloud-based service. There, demanding computations are outsourced in order to limit infrastructure costs. The idea of verifiable computing is to associate a data structure, a proof-of-work certificate, to the result of the outsourced computation. This allows a verification algorithm to prove the validity of the result, faster than by recomputing it. We talk about a Prover (the server performing the computations) and a Verifier. Goldwasser, Kalai and Rothblum gave in 2008 a generic method to verify any parallelizable computation, in almost linear time in the size of the, potentially structured, inputs and the result. However, the extra cost of the computations for the Prover (and therefore the extra cost to the customer), although only almost a constant factor of the overall work, is nonetheless prohibitive in practice. Differently, we will here present problem-specific procedures in computer algebra, e.g. for exact linear algebra computations, that are Prover-optimal, that is that have much less financial overhead.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
