{"id":77,"date":"2011-06-07T23:27:07","date_gmt":"2011-06-07T23:27:07","guid":{"rendered":"http:\/\/homepages.inf.ed.ac.uk\/jdf\/?page_id=77"},"modified":"2021-10-27T08:05:40","modified_gmt":"2021-10-27T08:05:40","slug":"projects-and-tools","status":"publish","type":"page","link":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/projects-and-tools\/","title":{"rendered":"Tools"},"content":{"rendered":"<p>Over the \u00a0years I have been involved in the creation of a number of AI reasoning systems and frameworks, and mechanized theories. These include (note: not up-to-date, see also our <a href=\"http:\/\/aiml.inf.ed.ac.uk\">AIML<\/a> web page):<\/p>\n<div>\n<ul>\n<li>Digiflow Tool (work with the WorkflowFM\/Digiflow team that includes P. Papapanagiotou, James Vaughan and Filip Smola). Following this project, we have recently released the following components of WorkfloFM as open source software <strong>(2021):<\/strong>\n<ul>\n<li><a href=\"http:\/\/docs.workflowfm.com\/workflowfm-reasoner\">WorkflowFM Reasoner\/Logic Engine<\/a> for correct-by-construction reasoning (in HOL Light).<\/li>\n<li><a href=\"https:\/\/github.com\/workflowfm\/workflowfm-composer\">WorkflowFM Visual Composer.<\/a><\/li>\n<\/ul>\n<\/li>\n<li>Archive of Formal Proof submission on mechanising <a href=\"https:\/\/www.isa-afp.org\/entries\/Schutz_Spacetime.html\">Schutz&#8217; Independent Axioms for Minkowski Spacetime<\/a> in Isabelle\/HOL. <strong>(2021)<\/strong><\/li>\n<li>An unofficial <a href=\"http:\/\/afp.theoremproving.org\">version<\/a> of the\u00a0Archive of Formal Proof (which is currently being incorporated into the official AFP) <strong>(2021).<\/strong>\n<ul>\n<li>Source code available <a href=\"https:\/\/github.com\/carlinmack\/afp\">here<\/a>.<\/li>\n<\/ul>\n<\/li>\n<li>Formalized theories of\u00a0<a href=\"https:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/library\/HOL\/HOL\/index.html\">Real and Complex analysis<\/a> in Isabelle\/HOL.<\/li>\n<li>The formalization of standard and<a href=\"https:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/library\/HOL\/HOL-Nonstandard_Analysis\/index.html\">\u00a0Nonstandard Analysis<\/a> in Isabelle\/HOL.<\/li>\n<li>A theorem proving framework for rigorous process modelling (ongoing work with P. Papapanagiotou in HOL Light).<\/li>\n<li>Idle-time Discovery Engines for Interactive Theorem Provers (work with P. Scott in HOL Light).<\/li>\n<li><a href=\"https:\/\/github.com\/jrh13\/hol-light\/tree\/master\/IsabelleLight\">Isabelle Light<\/a>, an Isabelle-like procedural language\/framework for HOL Light (with P. Papapanagiotou).<\/li>\n<li><a href=\"https:\/\/github.com\/jrh13\/hol-light\/tree\/master\/Boyer_Moore\">Boyer-Moore<\/a> Inductive Proof Tool for HOL-Light (with P. Papapanagiotou).<\/li>\n<li>The Prover&#8217;s Palette: An Eclipse IDE for Isabelle that integrates external tools around \u00a0the user (with L. Meikle).<\/li>\n<li><a href=\"https:\/\/homepages.inf.ed.ac.uk\/jdf\/geometry-explorer\/\">Geometry Explorer<\/a>, a system that combines dynamic geometry, automated geometry theorem proving, and diagrammatic proofs (with S. Wilson).<\/li>\n<li><a href=\"https:\/\/dream.inf.ed.ac.uk\/projects\/isaplanner\/\">IsaPlanner<\/a>, a proof-planning system implemented as part of Isabelle. The project was initiated under my EPSRC Grant\u00a0GR\/N37414 and then supported by the Mathematical Reasoning Group Platform Grant.<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Over the \u00a0years I have been involved in the creation of a number of AI reasoning systems and frameworks, and mechanized theories. These include (note: not up-to-date, see also our AIML web page): Digiflow Tool (work with the WorkflowFM\/Digiflow team &hellip; <a href=\"https:\/\/homepages.inf.ed.ac.uk\/jdf\/projects-and-tools\/\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":208,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-77","page","type-page","status-publish","has-post-thumbnail","hentry"],"_links":{"self":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages\/77","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/comments?post=77"}],"version-history":[{"count":34,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages\/77\/revisions"}],"predecessor-version":[{"id":519,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages\/77\/revisions\/519"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/media\/208"}],"wp:attachment":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/media?parent=77"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}