Billy Woods | Searcharxiv

arXiv2025

Capturing properties of planar diagrams in Lean proof assistant software

Automated proof assistants are a technology pre-empting mistakes in mathematics. In our practice we have seen that reasoning about planar diagrams is difficult to both humans and computers. One example that has led to wrong statements in publications is that an orientation-preserving mapping is not always defined by how it acts on triples of elements. In this paper we formalise orientation-preserving mappings in proof assistant software Lean and report on our take-aways.

math.CO↗

arXiv2023

Monomial methods in iterated local skew power series rings

Let $A = \mathbb{F}_p$ or $\mathbb{Z}_p$, and let $R = A[[x_1]][[x_2; σ_2, δ_2]]\dots[[x_n;σ_n,δ_n]]$, an iterated local skew power series ring over $A$. Under mild conditions, we show that (multiplicative) monomial orders exist, and develop the theory of Gröbner bases for $R$. We show that all rank-2 local skew power series rings over $\mathbb{F}_p$ satisfy polynormality, and give an example of a rank-2 local skew power series ring over $\mathbb{Z}_p$ which is a unique factorisation domain in the sense of Chatters-Jordan.

math.RA↗

arXiv2018

Mechanomyography based closed-loop Functional Electrical Stimulation cycling system

Functional Electrical Stimulation (FES) systems are successful in restoring motor function and supporting paralyzed users. Commercially available FES products are open loop, meaning that the system is unable to adapt to changing conditions with the user and their muscles which results in muscle fatigue and poor stimulation protocols. This is because it is difficult to close the loop between stimulation and monitoring of muscle contraction using adaptive stimulation. FES causes electrical artefacts which make it challenging to monitor muscle contractions with traditional methods such as electromyography (EMG). We look to overcome this limitation by combining FES with novel mechanomyographic (MMG) sensors to be able to monitor muscle activity during stimulation in real time. To provide a meaningful task we built an FES cycling rig with a software interface that enabled us to perform adaptive recording and stimulation, and then combine this with sensors to record forces applied to the pedals using force sensitive resistors (FSRs), crank angle position using a magnetic incremental encoder and inputs from the user using switches and a potentiometer. We illustrated this with a closed-loop stimulation algorithm that used the inputs from the sensors to control the output of a programmable RehaStim 1 FES stimulator (Hasomed) in real-time. This recumbent bicycle rig was used as a testing platform for FES cycling. The algorithm was designed to respond to a change in requested speed (RPM) from the user and change the stimulation power (% of maximum current mA) until this speed was achieved and then maintain it.

cs.RO↗