Future exploratory missions to the Moon and to Mars will involve solar-powered rovers; careful vehicle energy management is critical to the success of such missions. This article describes a unique ...dataset gathered by a small, four-wheeled rover at a planetary analog test facility in Canada. The rover was equipped with a suite of sensors designed to enable the study of energy-aware navigation and path planning algorithms. The sensors included a colour omnidirectional stereo camera, a monocular camera, an inertial measurement unit, a pyranometer, drive power consumption monitors, wheel encoders, and a GPS receiver. In total, the rover drove more than 1.2 km over varied terrain at the analog test site. All data is presented in human-readable text files and as standard-format images; additional Robot Operating System (ROS) parsing tools and several georeferenced aerial maps of the test environment are also included. A series of potential research use cases is described.
In order to apply canonical labelling of graphs and isomorphism checking in
interactive theorem provers, these checking algorithms must either be
mechanically verified or their results must be ...verifiable by independent
checkers. We analyze a state-of-the-art algorithm for canonical labelling of
graphs (described by McKay and Piperno) and formulate it in terms of a formal
proof system. We provide an implementation that can export a proof that the
obtained graph is the canonical form of a given graph. Such proofs are then
verified by our independent checker and can be used to confirm that two given
graphs are not isomorphic.
We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line
C
P
1
and is shown to ...satisfy Tarski’s axioms except for Euclid’s axiom—it is shown to satisfy it’s negation, and, moreover, to satisfy the existence of limiting parallels axiom.
Articulated robots such as manipulators increasingly must operate in uncertain and dynamic environments where interaction (with human coworkers, for example) is necessary. In these situations, the ...capacity to quickly adapt to unexpected changes in operational space constraints is essential. At certain points in a manipulator’s configuration space, termed singularities, the robot loses one or more degrees of freedom (DoF) and is unable to move in specific operational space directions. The inability to move in arbitrary directions in operational space compromises adaptivity and, potentially, safety. We introduce a geometry-aware singularity index, defined using a Riemannian metric on the manifold of symmetric positive definite matrices, to provide a measure of proximity to singular configurations. We demonstrate that our index avoids some of the failure modes and difficulties inherent to other common indices. Further, we show that our index can be differentiated easily, making it compatible with local optimization approaches used for operational space control. Our experimental results establish that, for reaching and path following tasks, optimization based on our index outperforms a common manipulability maximization technique and ensures singularity-robust motions.
•A singularity index based on the geodesic connecting two manipulability ellipsoids.•Geometric interpretations of the proposed index applied to singularity avoidance.•Proof that the proposed index can be differentiated.•An operational space tracking formulation for singularity avoidance.
We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most ...state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle’s built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver.
We describe a system for automated ruler and compass triangle constructions in hyperbolic geometry. We discuss key differences between constructions in Euclidean and hyperbolic setting, compile a ...list of primitive constructions and lemmas used for constructions in hyperbolic geometry, build an automated system for solving construction problems, and test it on a corpus of triangle-construction problems. We extend the list of primitive constructions for hyperbolic geometry by several constructions that cannot be done by ruler and compass, but can be done by using algebraic calculations and show that such extended system solves more problems. We also use a dynamic geometry library to build an online compendium containing construction descriptions, illustrations, and step-by-step animations.
•CC systems are abstract representations of point triples orientation in a plane.•The number of non-isomorphic CC systems grows very fast with more points added.•Enumeration of CC systems is useful ...in proving discrete geometry conjectures.•Non-isomorphic CC systems of up to 12 points are re-enumerated using a new approach.
Donald Knuth introduced abstract CC systems to represent configurations of points in a plane with a given orientation (clockwise or counterclockwise) of all triples of points. We present efficient enumeration of all non-isomorphic CC systems with at most 12 points. Our algorithm is based on Faradžev-Read type enumeration, enhanced with the homomorphism principle and SAT solving, enabling us to enumerate more than 1.3⋅1012 non-isomorphic CC systems with 12 points.
Most, if not all, state-of-the-art complete SAT solvers are complex variations of the DPLL procedure described in the early 1960’s. Published descriptions of these modern algorithms and related data ...structures are given either as high-level state transition systems or, informally, as (pseudo) programming language code. The former, although often accompanied with (informal) correctness proofs, are usually very abstract and do not specify many details crucial for efficient implementation. The latter usually do not involve any correctness argument and the given code is often hard to understand and modify. This paper aims to bridge this gap by presenting SAT solving algorithms that are formally proved correct and also contain information required for efficient implementation. We use a tutorial, top-down, approach and develop a SAT solver, starting from a simple design that is subsequently extended, step-by-step, with a requisite series of features. The heuristic parts of the solver are abstracted away, since they usually do not affect solver correctness (although they are very important for efficiency). All algorithms are given in pseudo-code and are accompanied with correctness conditions, given in Hoare logic style. The correctness proofs are formalized within the Isabelle theorem proving system and are available in the extended version of this paper. The given pseudo-code served as a basis for our SAT solver
argo-sat
.
PDF
