-
MyWeekInSight: Designing and Evaluating the Use of Visualization in Self-Management of Chronic Pain by Youth
Authors:
Unma Desai,
Haley Foladare,
Katelynn E. Boerner,
Tim F. Oberlander,
Tamara Munzner,
Karon E. MacLean
Abstract:
A teenager's experience of chronic pain reverberates through multiple interacting aspects of their lives. To self-manage their symptoms, they need to understand how factors such as their sleep, social interactions, emotions and pain intersect; supporting this capability must underlie an effective personalized healthcare solution. While adult use of personal informatics for self-management of vario…
▽ More
A teenager's experience of chronic pain reverberates through multiple interacting aspects of their lives. To self-manage their symptoms, they need to understand how factors such as their sleep, social interactions, emotions and pain intersect; supporting this capability must underlie an effective personalized healthcare solution. While adult use of personal informatics for self-management of various health factors has been studied, solutions intended for adults are rarely workable for teens, who face this complex and confusing situation with unique perspectives, skills and contexts. In this design study, we explore a means of facilitating self-reflection by youth living with chronic pain, through visualization of their personal health data. In collaboration with pediatric chronic pain clinicians and a health-tech industry partner, we designed and deployed MyWeekInSight, a visualization-based self-reflection tool for youth with chronic pain. We discuss our staged design approach with this intersectionally vulnerable population, in which we balanced reliance on proxy users and data with feedback from youth viewing their own data. We report on extensive formative and in-situ evaluation, including a three-week clinical deployment, and present a framework of challenges and barriers faced in clinical deployment with mitigations that can aid fellow researchers. Our reflections on the design process yield principles, surprises, and open questions.
△ Less
Submitted 30 May, 2024;
originally announced May 2024.
-
The Imandra Automated Reasoning System (system description)
Authors:
Grant Olney Passmore,
Simon Cruanes,
Denis Ignatovich,
Dave Aitken,
Matt Bray,
Elijah Kagan,
Kostya Kanishev,
Ewen Maclean,
Nicola Mometto
Abstract:
We describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision procedures such as SMT, semi-automatic inductive provers of the Boyer-Moore family like ACL2, and interactive proof assistants for typed higher-order logics. Imandra's logic is computational, based on a pure subset of OCaml in which all functions are terminating, with restrictions on types…
▽ More
We describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision procedures such as SMT, semi-automatic inductive provers of the Boyer-Moore family like ACL2, and interactive proof assistants for typed higher-order logics. Imandra's logic is computational, based on a pure subset of OCaml in which all functions are terminating, with restrictions on types and higher-order functions that allow conjectures to be translated into multi-sorted first-order logic with theories, including arithmetic and datatypes. Imandra has novel features supporting large-scale industrial applications, including a seamless integration of bounded and unbounded verification, first-class computable counterexamples, efficiently executable models and a cloud-native architecture supporting live multiuser collaboration.
The core reasoning mechanisms of Imandra are (i) a semi-complete procedure for finding models of formulas in the logic mentioned above, centered around the lazy expansion of recursive functions, and (ii) an inductive waterfall and simplifier which "lifts" many Boyer-Moore ideas to our typed higher-order setting.
These mechanisms are tightly integrated and subject to many forms of user control. Imandra's user interfaces include an interactive toplevel, Jupyter notebooks and asynchronous document-based verification (in the spirit of Isabelle's Prover IDE) with VS Code.
△ Less
Submitted 21 April, 2020;
originally announced April 2020.
-
Fully Automated Myocardial Strain Estimation from CMR Tagged Images using a Deep Learning Framework in the UK Biobank
Authors:
Edward Ferdian,
Avan Suinesiaputra,
Kenneth Fung,
Nay Aung,
Elena Lukaschuk,
Ahmet Barutcu,
Edd Maclean,
Jose Paiva,
Stefan K. Piechnik,
Stefan Neubauer,
Steffen E Petersen,
Alistair A. Young
Abstract:
Purpose: To demonstrate the feasibility and performance of a fully automated deep learning framework to estimate myocardial strain from short-axis cardiac magnetic resonance tagged images. Methods and Materials: In this retrospective cross-sectional study, 4508 cases from the UK Biobank were split randomly into 3244 training and 812 validation cases, and 452 test cases. Ground truth myocardial lan…
▽ More
Purpose: To demonstrate the feasibility and performance of a fully automated deep learning framework to estimate myocardial strain from short-axis cardiac magnetic resonance tagged images. Methods and Materials: In this retrospective cross-sectional study, 4508 cases from the UK Biobank were split randomly into 3244 training and 812 validation cases, and 452 test cases. Ground truth myocardial landmarks were defined and tracked by manual initialization and correction of deformable image registration using previously validated software with five readers. The fully automatic framework consisted of 1) a convolutional neural network (CNN) for localization, and 2) a combination of a recurrent neural network (RNN) and a CNN to detect and track the myocardial landmarks through the image sequence for each slice. Radial and circumferential strain were then calculated from the motion of the landmarks and averaged on a slice basis. Results: Within the test set, myocardial end-systolic circumferential Green strain errors were -0.001 +/- 0.025, -0.001 +/- 0.021, and 0.004 +/- 0.035 in basal, mid, and apical slices respectively (mean +/- std. dev. of differences between predicted and manual strain). The framework reproduced significant reductions in circumferential strain in diabetics, hypertensives, and participants with previous heart attack. Typical processing time was ~260 frames (~13 slices) per second on an NVIDIA Tesla K40 with 12GB RAM, compared with 6-8 minutes per slice for the manual analysis. Conclusions: The fully automated RNNCNN framework for analysis of myocardial strain enabled unbiased strain evaluation in a high-throughput workflow, with similar ability to distinguish impairment due to diabetes, hypertension, and previous heart attack.
△ Less
Submitted 15 April, 2020;
originally announced April 2020.
-
The Search for Computational Intelligence
Authors:
Joseph Corneli,
Ewen Maclean
Abstract:
We define and explore in simulation several rules for the local evolution of generative rules for 1D and 2D cellular automata. Our implementation uses strategies from conceptual blending. We discuss potential applications to modelling social dynamics.
We define and explore in simulation several rules for the local evolution of generative rules for 1D and 2D cellular automata. Our implementation uses strategies from conceptual blending. We discuss potential applications to modelling social dynamics.
△ Less
Submitted 31 January, 2015;
originally announced February 2015.
-
Proof-Pattern Recognition and Lemma Discovery in ACL2
Authors:
Jónathan Heras,
Ekaterina Komendantskaya,
Moa Johansson,
Ewen Maclean
Abstract:
We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition to pre-processes data from libraries, and then suggests auxiliary lemmas in new proofs by analogy with already seen examples. This paper presents the implement…
▽ More
We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition to pre-processes data from libraries, and then suggests auxiliary lemmas in new proofs by analogy with already seen examples. This paper presents the implementation of ACL2(ml) alongside theoretical descriptions of the proof-pattern recognition and lemma discovery methods involved in it.
△ Less
Submitted 15 October, 2013; v1 submitted 8 August, 2013;
originally announced August 2013.
-
Towards Automated Proof Strategy Generalisation
Authors:
Gudmund Grov,
Ewen Maclean
Abstract:
The ability to automatically generalise (interactive) proofs and use such generalisations to discharge related conjectures is a very hard problem which remains unsolved. Here, we develop a notion of goal types to capture key properties of goals, which enables abstractions over the specific order and number of sub-goals arising when composing tactics. We show that the goal types form a lattice, and…
▽ More
The ability to automatically generalise (interactive) proofs and use such generalisations to discharge related conjectures is a very hard problem which remains unsolved. Here, we develop a notion of goal types to capture key properties of goals, which enables abstractions over the specific order and number of sub-goals arising when composing tactics. We show that the goal types form a lattice, and utilise this property in the techniques we develop to automatically generalise proof strategies in order to reuse it for proofs of related conjectures. We illustrate our approach with an example.
△ Less
Submitted 9 June, 2013; v1 submitted 12 March, 2013;
originally announced March 2013.
