Differences in muscle activity during hand dexterity tasks between women with arthritis and a healthy reference group

Background. Impaired hand function is common in patients with arthritis and it affects performance of daily activities; thus, hand exercises are recommended. There is little information on the extent to which the disease affects activation of the flexor and extensor muscles during these hand-dexterity tasks. The purpose of this study was to compare muscle activation during such tasks in subjects with arthritis and in a healthy reference group. Methods. Muscle activation was measured in m. extensor digitorium communis (EDC) and in m. flexor carpi radialis (FCR) with surface electromyography (EMG) in women with rheumatoid arthritis (RA, n = 20), hand osteoarthritis (HOA, n = 16) and in a healthy reference group (n = 20) during the performance of four daily activity tasks and four hand exercises. Maximal voluntary isometric contraction (MVIC) was measured to enable intermuscular comparisons, and muscle activation is presented as %MVIC. Results. The arthritis group used a higher %MVIC than the reference group in both FCR and EDC when cutting with a pair of scissors, pulling up a zipper and—for the EDC—also when writing with a pen and using a key (p < 0.02). The exercise “rolling dough with flat hands” required the lowest %MVIC and may be less effective in improving muscle strength. Conclusions. Women with arthritis tend to use higher levels of muscle activation in daily tasks than healthy women, and wrist extensors and flexors appear to be equally affected. It is important that hand training programs reflect real-life situations and focus also on extensor strength.

Fred: An approach to generating real, correct, reusable programs from proofs

In this paper we describe our system for automatically extracting "correct" programs from proofs using a development of the Curry-Howard process. Although program extraction has been developed by many authors, our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique to reduce higher-order logic to many-sorted (first-order) logic; 2. the free use of new rules for induction subject to certain conditions; 3. the extensive use of previously programmed (total, recursive) functions; 4. the use of templates to make the reasoning much closer to normal mathematical proofs and 5. a conceptual distinction between the computational type theory (for representing programs)and the logical type theory (for reasoning about programs). As an example of our system we give a constructive proof of the well known theorem that every graph of even parity, which is non-trivial in the sense that it does not consist of isolated vertices, has a cycle. Given such a graph as input, the extracted program produces a cycle as promised.

Protocols between programs and proofs

In this paper we describe a new protocol that we call the Curry-Howard protocol between a theory and the programs extracted from it. This protocol leads to the expansion of the theory and the production of more powerful programs. The methodology we use for automatically extracting “correct” programs from proofs is a development of the well-known Curry-Howard process. Program extraction has been developed by many authors, but our presentation is ultimately aimed at a practical, usable system and has a number of novel features. These include 1. a very simple and natural mimicking of ordinary mathematical practice and likewise the use of established computer programs when we obtain programs from formal proofs, and 2. a conceptual distinction between programs on the one hand, and proofs of theorems that yield programs on the other. An implementation of our methodology is the Fred system. As an example of our protocol we describe a constructive proof of the well-known theorem that every graph of even parity can be decomposed into a list of disjoint cycles. Given such a graph as input, the extracted program produces a list of the (non-trivial) disjoint cycles as promised.

Extraction of structured programs from specification proofs

We present a method using an extended logical system for obtaining programs from specifications written in a sublanguage of CASL. These programs are “correct” in the sense that they satisfy their specifications. The technique we use is to extract programs from proofs in formal logic by techniques due to Curry and Howard. The logical calculus, however, is novel because it adds structural rules corresponding to the standard ways of modifying specifications: translating (renaming), taking unions, and hiding signatures. Although programs extracted by the Curry-Howard process can be very cumbersome, we use a number of simplifications that ensure that the programs extracted are in a language close to a standard high-level programming language. We use this to produce an executable refinement of a given specification and we then provide a method for producing a program module that maximally respects the original structure of the specification. Throughout the paper we demonstrate the technique with a simple example.