Pappus’s Hexagon Theorem in Real Projective PlaneThis work has been supported by the “Centre autonome de formation et de recherche en mathématiques et sciences avec assistants de preuve” ASBL (non-profit organization). Enterprise number: 0777.779.751. Belgium.

Summary. In this article we prove, using Mizar [2], [1], the Pappus’s hexagon theorem in the real projective plane: “Given one set of collinear points A, B, C, and another set of collinear points a, b, c, then the intersection points X, Y, Z of line pairs Ab and aB, Ac and aC, Bc and bC are collinear” https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem . More precisely, we prove that the structure ProjectiveSpace TOP-REAL3 [10] (where TOP-REAL3 is a metric space defined in [5]) satisfies the Pappus’s axiom defined in [11] by Wojciech Leończuk and Krzysztof Prażmowski. Eugeniusz Kusak and Wojciech Leończuk formalized the Hessenberg theorem early in the MML [9]. With this result, the real projective plane is Desarguesian. For proving the Pappus’s theorem, two different proofs are given. First, we use the techniques developed in the section “Projective Proofs of Pappus’s Theorem” in the chapter “Pappos’s Theorem: Nine proofs and three variations” [12]. Secondly, Pascal’s theorem [4] is used. In both cases, to prove some lemmas, we use Prover9 https://www.cs.unm.edu/~mccune/prover9/ , the successor of the Otter prover and ott2miz by Josef Urban See its homepage https://github.com/JUrban/ott2miz [13], [8], [7]. In Coq, the Pappus’s theorem is proved as the application of Grassmann-Cayley algebra [6] and more recently in Tarski’s geometry [3].

Classification of 3T1R Parallel Manipulators Based on Their Wrench Graph

This paper presents a classification of 3T1R parallel manipulators (PMs) based on the wrench graph. By using the theory of reciprocal screws, the properties of the three-dimensional projective space, the wrench graph, and the superbracket decomposition of Grassmann–Cayley algebra, six typical wrench graphs for 3T1R parallel manipulators are obtained along with their singularity conditions. Furthermore, this paper shows a way in which each of the obtained typical wrench graphs can be used in order to synthesize new 3T1R parallel manipulator architectures with known singularity conditions and with an understanding of their geometrical properties and assembly conditions.

On the consistency problem for modular lattices and related structures

The consistency problem for a class of algebraic structures asks for an algorithm to decide, for any given conjunction of equations, whether it admits a non-trivial satisfying assignment within some member of the class. For the variety of all groups, this is the complement of the triviality problem, shown undecidable by by Adyan [Algorithmic unsolvability of problems of recognition of certain properties of groups. (Russian) Dokl. Akad. Nauk SSSR (N.S.) 103 (1955) 533–535] and Rabin [Recursive unsolvability of group theoretic problems, Ann. of Math. (2) 67 (1958) 172–194]. For the class of finite groups, it amounts to the triviality problem for profinite completions, shown undecidable by Bridson and Wilton [The triviality problem for profinite completions, Invent. Math. 202 (2015) 839–874]. We derive unsolvability of the consistency problem for the class of (finite) modular lattices and various subclasses; in particular, the class of all subspace lattices of finite-dimensional vector spaces over a fixed or arbitrary field of characteristic [Formula: see text] and expansions thereof, e.g. the class of subspace ortholattices of finite-dimensional Hilbert spaces. The lattice results are used to prove unsolvability of the consistency problem for (finite) rings with unit and (finite) representable relation algebras. These results in turn apply to equations between simple expressions in Grassmann–Cayley algebra and to functional and embedded multivalued dependencies in databases.

A geometric approach for singularity analysis of 3-DOF planar parallel manipulators using Grassmann–Cayley algebra

SUMMARYSingular configurations of parallel manipulators (PMs) are special poses in which the manipulators cannot maintain their inherent infinite rigidity. These configurations are very important because they prevent the manipulator from being controlled properly, or the manipulator could be damaged. A geometric approach is introduced to identify singular conditions of planar parallel manipulators (PPMs) in this paper. The approach is based on screw theory, Grassmann–Cayley Algebra (GCA), and the static Jacobian matrix. The static Jacobian can be obtained more easily than the kinematic ones in PPMs. The Jacobian is expressed and analyzed by the join and meet operations of GCA. The singular configurations can be divided into three classes. This approach is applied to ten types of common PPMs consisting of three identical legs with one actuated joint and two passive joints.

Combinatorial Method for Characterizing Singular Configurations in Parallel Mechanisms

The paper presents a method for finding the different singular configurations of several types of parallel mechanisms/robots using the combinatorial method. The main topics of the combinatorial method being used are: equimomental line/screw, self-stresses, Dual Kennedy theorem and circle, and various types of 2D and 3D Assur Graphs such as: triad, tetrad and double triad. The paper introduces combinatorial characterization of 3/6 SP and compares it to singularity analysis of 3/6 SP using Grassmann Line Geometry and Grassmann-Cayley Algebra. Finally, the proposed method is applied for characterizing the singular configurations of more complex parallel mechanisms such as 3D tetrad and 3D double-triad.