arXiv subjects

Stephan Schulz

Publications and source records attributed to Stephan Schulz.

8 recordsLinked to original sources

arXiv2026

Some Experiments with Twee-Style Goal-Directedness

In saturation-based theorem proving, selecting the next clause for processing is a major concern. Twee has successfully applied the idea of preferring clauses that share terms with the conjecture by adding equational definitions to transform the problem. In this paper, we apply the idea to the full first-order case, and offer an alternative implementation based on shared terms. Both approaches have complementary applications and show very promising results.

cs.LO↗

arXiv2026

A Local Probe Mass Spectrometer for Localized and Sensitive Product Detection in Environmental Electron Microscopy

Aberration-corrected environmental transmission electron microscopy (ETEM) enables atomic-resolution imaging of dynamic catalytic processes. Correlating atomic-scale structural changes with reaction products detected by mass spectrometry offers a powerful route to uncover catalytic mechanisms. However, current approaches face fundamental limitations: closed-cell ETEM setups suffer from diffuse scattering by SiN windows, degrading spatial resolution and sensitivity, while open-cell configurations enable high-resolution imaging and maintain high sensitivity but suffer from significant dilution of reaction products during transport to the mass spectrometer (MS). To overcome these challenges, we develop a Local Probe Mass Spectrometer (LPMS) integrated with aberration-corrected ETEM. The setup combines a DENSsolution Stream holder with a MS. To preserve spatial resolution, both top and bottom SiN membranes of the MEMS chip are removed, while the gas environment is maintained via the ETEM chamber. Reaction products are sampled locally via a micro-capillary positioned near the catalyst and connected to a holder gas line that delivers the gas to the MS. Initial validation in environmental SEM confirmed controlled gas delivery to the MS. Co3O4 nanoplates serve as a model catalyst due to their inherent electron transparency, enabling atomic-resolution imaging without FIB lamella preparation and associated ion-beam damage. A novel micro-shuttle transfer strategy enables controlled placement of a defined number of nanoplates at the reaction site with precise crystallographic orientation. This establishes the foundation for quantitative structure reactivity correlation by enabling simultaneous, spatially resolved detection of reaction products and atomic-scale structural dynamics.

cond-mat.mtrl-sci↗

arXiv2026

Case Study: Saturations as Explicit Models in Equational Theories

Automated theorem provers (ATPs) can disprove conjectures by saturating a set of clauses, but the resulting saturated sets are opaque certificates. In the unit equational fragment, a saturated set can in fact be read as a convergent rewrite system defining an explicit, possibly infinite, model -- but this is not widely known, even amongst frequent users of ATPs. Moreover, ATPs do not emit these explicit certificates for infinite (counter-)models. We present such a certificate construction in full, implement it in Vampire and E, and apply it to the recent Equational Theories Project, where hundreds of implications do not admit finite countermodels. The resulting rewrite systems can be checked for confluence and termination by existing certified tools, yielding trustworthy countermodels.

cs.LO↗

arXiv2023

MizAR 60 for Mizar 50

As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60\% of the Mizar theorems in the hammer setting. We also automatically prove 75\% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.

cs.AI↗

arXiv2018

ProofWatch: Watchlist Guidance for Large Theories in E

Watchlist (also hint list) is a mechanism that allows related proofs to guide a proof search for a new conjecture. This mechanism has been used with the Otter and Prover9 theorem provers, both for interactive formalizations and for human-assisted proving of open conjectures in small theories. In this work we explore the use of watchlists in large theories coming from first-order translations of large ITP libraries, aiming at improving hammer-style automation by smarter internal guidance of the ATP systems. In particular, we (i) design watchlist-based clause evaluation heuristics inside the E ATP system, and (ii) develop new proof guiding algorithms that load many previous proofs inside the ATP and focus the proof search using a dynamically updated notion of proof matching. The methods are evaluated on a large set of problems coming from the Mizar library, showing significant improvement of E's standard portfolio of strategies, and also of the previous best set of strategies invented for Mizar by evolutionary methods.

cs.AI↗

arXiv2008

New results on rewrite-based satisfiability procedures

Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in theory T. If a sound and complete inference system for first-order logic is guaranteed to terminate on T-satisfiability problems, any theorem-proving strategy with that system and a fair search plan is a T-satisfiability procedure. We prove termination of a rewrite-based first-order engine on the theories of records, integer offsets, integer offsets modulo and lists. We give a modularity theorem stating sufficient conditions for termination on a combinations of theories, given termination on each. The above theories, as well as others, satisfy these conditions. We introduce several sets of benchmarks on these theories and their combinations, including both parametric synthetic benchmarks to test scalability, and real-world problems to test performances on huge sets of literals. We compare the rewrite-based theorem prover E with the validity checkers CVC and CVC Lite. Contrary to the folklore that a general-purpose prover cannot compete with reasoners with built-in theories, the experiments are overall favorable to the theorem prover, showing that not only the rewriting approach is elegant and conceptually simple, but has important practical implications.

cs.AI↗

arXiv2008

Sideband cooling and coherent dynamics in a microchip multi-segmented ion trap

Miniaturized ion trap arrays with many trap segments present a promising architecture for scalable quantum information processing. The miniaturization of segmented linear Paul traps allows partitioning the microtrap in different storage and processing zones. The individual position control of many ions - each of them carrying qubit information in its long-lived electronic levels - by the external trap control voltages is important for the implementation of next generation large-scale quantum algorithms. We present a novel scalable microchip multi-segmented ion trap with two different adjacent zones, one for the storage and another dedicated for the processing of quantum information using single ions and linear ion crystals: A pair of radio-frequency driven electrodes and 62 independently controlled DC electrodes allows shuttling of single ions or linear ion crystals with numerically designed axial potentials at axial and radial trap frequencies of a few MHz. We characterize and optimize the microtrap using sideband spectroscopy on the narrow S1/2 <-> D5/2 qubit transition of the 40Ca+ ion, demonstrate coherent single qubit Rabi rotations and optical cooling methods. We determine the heating rate using sideband cooling measurements to the vibrational ground state which is necessary for subsequent two-qubit quantum logic operations. The applicability for scalable quantum information processing is proven.

quant-ph↗

arXiv2006

Optimization of segmented linear Paul traps and transport of stored particles

Single ions held in linear Paul traps are promising candidates for a future quantum computer. Here, we discuss a two-layer microstructured segmented linear ion trap. The radial and axial potentials are obtained from numeric field simulations and the geometry of the trap is optimized. As the trap electrodes are segmented in the axial direction, the trap allows the transport of ions between different spatial regions. Starting with realistic numerically obtained axial potentials, we optimize the transport of an ion such that the motional degrees of freedom are not excited, even though the transport speed far exceeds the adiabatic regime. In our optimization we achieve a transport within roughly two oscillation periods in the axial trap potential compared to typical adiabatic transports that take of the order 100 oscillations. Furthermore heating due to quantum mechanical effects is estimated and suppression strategies are proposed.

quant-ph↗