{"id":3946,"date":"2013-12-23T08:11:24","date_gmt":"2013-12-23T07:11:24","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3946"},"modified":"2013-12-23T08:18:57","modified_gmt":"2013-12-23T07:18:57","slug":"formal-kinematic-analysis-of-the-two-link-planar-manipulator","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formal-kinematic-analysis-of-the-two-link-planar-manipulator\/","title":{"rendered":"Formal kinematic analysis of the two-link planar manipulator"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/\">HOL Light<\/a> sobre cinem\u00e1tica titulado <a href=\"http:\/\/save.seecs.nust.edu.pk\/pubs\/ICFEM_2013.pdf\">Formal kinematic analysis of the two-link planar manipulator<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/save.seecs.nust.edu.pk\/students\/binyameen\/tlpm.html\">Binyameen Farooq<\/a>, <a href=\"http:\/\/ohasan.seecs.nust.edu.pk\">Osman Hasan<\/a>, <a href=\"http:\/\/seecs.nust.edu.pk\/faculty\/sohail.html\">Sohail Iqbal<\/a> (de la Universidad de Islamabad, Pakist\u00e1n).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nKinematic analysis is used for trajectory planning of robotic manipulators and is an integral step of their design. The main idea behind kinematic analysis is to study the motion of the robot based on the geometrical relationship of the robotic links and their joints. Given the continuous nature of kinematic analysis, traditional computer-based verification methods, such as simulation, numerical methods or model checking, fail to provide reliable results. This fact makes robotic designs error prone, which may lead to disastrous consequences given the safety-critical nature of robotic applications. Leveraging upon the high expressiveness of higher-order logic, we propose to use higher-order-logic theorem proving for conducting formal kinematic analysis. As a first step towards this direction, we utilize the geometry theory of HOL-Light to develop formal reasoning support for the kinematic analysis of a two-link planar manipulator, which forms the basis for many mechanical structures in robotics. To illustrate the usefulness of our foundational formalization, we present the formal kinematic analysis of a biped walking robot.\n<\/p><\/blockquote>\n<p>El trabajo se ha presentado en el <a href=\"https:\/\/www.cs.auckland.ac.nz\/research\/conferences\/icfem2013\/\">ICFEM 2013<\/a> (<i>15th International Conference on Formal Engineering Methods<\/i>). Las trasparencias de la presentaci\u00f3n se encuentran <a href=\"http:\/\/bit.ly\/J8jLkS\">aqu\u00ed<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en HOL LIght se encuentra <a href=\"http:\/\/save.seecs.nust.edu.pk\/students\/binyameen\/tlpm.html\">aqu\u00ed<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en HOL Light sobre cinem\u00e1tica titulado Formal kinematic analysis of the two-link planar manipulator. Sus autores son Binyameen Farooq, Osman Hasan, Sohail Iqbal (de la Universidad de Islamabad, Pakist\u00e1n). Su resumen es Kinematic analysis is used for trajectory planning of robotic manipulators and is an integral step&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[22,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3946"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3946"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3946\/revisions"}],"predecessor-version":[{"id":3949,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3946\/revisions\/3949"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3946"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3946"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3946"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}