Concept
Proof by exhaustion
Related publications (36)
LISA – A Modern Proof System
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir
We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...
2023A proof of the instability of AdS for the Einstein-massless Vlasov system
In recent years, the conjecture on the instability of Anti-de Sitter spacetime, put forward by Dafermos-Holzegel (Dynamic instability of solitons in 4 + 1 dimesnional gravity with negative cosmological constant, 2006. https://www.dpmms.cam.ac.uk/similar to ...
SPRINGER HEIDELBERG2022Convex Quantization Preserves Logconcavity
A logconcave likelihood is as important to proper statistical inference as a convex cost function is important to variational optimization. Quantization is often disregarded when writing likelihood models, ignoring the limitations of the physical detectors ...
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2022Switchover phenomenon induced by epidemic seeding on geometric networks
It is a fundamental question in disease modeling how the initial seeding of an epidemic, spreading over a network, determines its final outcome. One important goal has been to find the seed configuration, which infects the most individuals. Although the id ...
2021Ultralow-noise photonic microwave synthesis using a soliton microcomb-based transfer oscillator
Tobias Kippenberg, Erwan Guillaume Albert Lucas
The synthesis of ultralow-noise microwaves is of both scientific and technological relevance for timing, metrology, communications and radio-astronomy. Today, the lowest reported phase noise signals are obtained via optical frequency-division using mode-lo ...
NATURE PUBLISHING GROUP2020