{"id":56,"date":"2015-06-16T13:44:07","date_gmt":"2015-06-16T11:44:07","guid":{"rendered":"http:\/\/members.loria.fr\/thierrygartiser\/?page_id=56"},"modified":"2018-11-23T18:19:47","modified_gmt":"2018-11-23T16:19:47","slug":"accueil","status":"publish","type":"page","link":"https:\/\/members.loria.fr\/IGnaedig\/","title":{"rendered":"From termination to  the halting problem&#8230;"},"content":{"rendered":"<p>I am interested in automated\u00a0deduction\u00a0problems. Coming from the rewriting community, I have worked on rewriting termination proofs and more generally on proofs of rewriting properties, in the context of rule-based programming.<\/p>\n<p>Putting now into perspective the inductive proof techniques I developed for equational theories, I am\u00a0studying the provability problem into axiomatic theories. Moving to proof theory, I am\u00a0investigating links between uncompleteness, undecidability and the halting problem.<\/p>\n<p>&nbsp;<\/p>\n<p><a href=\"\/IGnaedig\/wp-content\/blogs.dir\/95\/files\/sites\/95\/2015\/06\/Moebius-escher.jpg\"><img loading=\"lazy\" decoding=\"async\" class=\"size-medium wp-image-284 aligncenter\" src=\"\/IGnaedig\/wp-content\/blogs.dir\/95\/files\/sites\/95\/2015\/06\/Moebius-escher-300x143.jpg\" alt=\"moebius-escher\" width=\"280\" height=\"133\" srcset=\"https:\/\/members.loria.fr\/IGnaedig\/wp-content\/blogs.dir\/95\/files\/sites\/95\/2015\/06\/Moebius-escher-300x143.jpg 300w, https:\/\/members.loria.fr\/IGnaedig\/wp-content\/blogs.dir\/95\/files\/sites\/95\/2015\/06\/Moebius-escher.jpg 326w\" sizes=\"auto, (max-width: 280px) 100vw, 280px\" \/><\/a><\/p>\n<p>&nbsp;<\/p>\n<p style=\"text-align: center\">My favourite theorem:<\/p>\n<p style=\"text-align: center\">Assume <i>F<\/i> is a consistent axiomatic\u00a0system which contains Robinson arithmetic.\u00a0Then a sentence <i>G<\/i><sub><i>F\u00a0<\/i><\/sub>of the language of <i>F<\/i> can be mechanically constructed from <i>F<\/i> such that\u00a0<i>F<\/i> \u22ac <i>G<\/i><sub><i>F \u00a0<\/i><\/sub>and\u00a0<i>F<\/i> \u22ac \u00ac<i>G<\/i><sub><i>F.<\/i><\/sub><\/p>\n<p style=\"text-align: right\"><em>Kurt G\u00f6del 1931<\/em><\/p>\n","protected":false},"excerpt":{"rendered":"<p>I am interested in automated\u00a0deduction\u00a0problems. Coming from the rewriting community, I have worked on rewriting termination proofs and more generally on proofs of rewriting properties, in the context of rule-based programming. Putting now into perspective the inductive proof techniques I developed for equational theories, I am\u00a0studying the provability problem into axiomatic theories. Moving to proof [&hellip;]<\/p>\n","protected":false},"author":5,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-56","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/members.loria.fr\/IGnaedig\/wp-json\/wp\/v2\/pages\/56","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/members.loria.fr\/IGnaedig\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/members.loria.fr\/IGnaedig\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/IGnaedig\/wp-json\/wp\/v2\/users\/5"}],"replies":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/IGnaedig\/wp-json\/wp\/v2\/comments?post=56"}],"version-history":[{"count":23,"href":"https:\/\/members.loria.fr\/IGnaedig\/wp-json\/wp\/v2\/pages\/56\/revisions"}],"predecessor-version":[{"id":325,"href":"https:\/\/members.loria.fr\/IGnaedig\/wp-json\/wp\/v2\/pages\/56\/revisions\/325"}],"wp:attachment":[{"href":"https:\/\/members.loria.fr\/IGnaedig\/wp-json\/wp\/v2\/media?parent=56"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}