arXiv subjects

Marcel Ullrich

Publications and source records attributed to Marcel Ullrich.

5 recordsLinked to original sources

arXiv2020

Generating induction principles and subterm relations for inductive types using MetaCoq

We implement three Coq plugins regarding inductive types in MetaCoq. The first plugin is a simple syntax transformation generating alternative constructors for inductive types by abstracting over concrete indices in the types of the constructors. The second plugin re-implements Coq's $\texttt{Scheme Induction}$ command in MetaCoq, and extends it to nested inductive types, e.g. types like rose trees which use $\texttt{list}$ in their definition, similar to the Elpi-plugin by Tassi. The third plugin implements the $\texttt{Derive Subterm}$ command provided by the Equations package in MetaCoq.

cs.LO↗

arXiv2018

Monotonicity based shape reconstruction in electrical impedance tomography

Current-voltage measurements in electrical impedance tomography can be partially ordered with respect to definiteness of the associated self-adjoint Neumann-to-Dirichlet operators (NtD). With this ordering, a point-wise larger conductivity leads to smaller current-voltage measurements, and smaller conductivities lead to larger measurements. We present a converse of this simple monotonicity relation and use it to solve the shape reconstruction (aka inclusion detection) problem in EIT. The outer shape of a region where the conductivity differs from a known background conductivity can be found by simply comparing the measurements to that of smaller or larger test regions.

math.NA↗

arXiv2018

Resolution Guarantees in Electrical Impedance Tomography

Electrical impedance tomography (EIT) uses current-voltage measurements on the surface of an imaging subject to detect conductivity changes or anomalies. EIT is a promising new technique with great potential in medical imaging and non-destructive testing. However, in many applications, EIT suffers from inconsistent reliability due to its enormous sensitivity to modeling and measurement errors. In this work we show that rigorous resolution guarantees are possible within a realistic EIT measurement setting including systematic and random errors. We derive a constructive criterion to decide whether a desired resolution can be achieved in a given measurement setup. Our result covers the detection of anomalies of a known minimal contrast using noisy measurements on a number of electrodes attached to a subject with imprecisely known background conductivity.

math.NA↗

arXiv2018

Local uniqueness for an inverse boundary value problem with partial data

In dimension $n\geq 3$, we prove a local uniqueness result for the potentials $q$ of the Schrödinger equation $-Δu+qu=0$ from partial boundary data. More precisely, we show that potentials $q_1,q_2\in L^\infty$ with positive essential infima can be distinguished by local boundary data if there is a neighborhood of a boundary part where $q_1\geq q_2$ and $q_1\not\equiv q_2$.

math.AP↗

arXiv2018

Combining frequency-difference and ultrasound modulated electrical impedance tomography

Electrical impedance tomography (EIT) is highly affected by modeling errors regarding electrode positions and the shape of the imaging domain. In this work, we propose a new inclusion detection technique that is completely independent of such errors. Our new approach is based on a combination of frequency-difference and ultrasound modulated EIT measurements.

math.AP↗