LogOS: models for AI-driven, human-on-the-loop, machine-checked formal reasoning
Abstract
This release contains extensive refactoring. A first goal was to make refinement take precedence over equality more. The result is more coherence in the system, and strictly more generality by removing artificial bottlenecks. A second was to thread the handling of inifinities better through the system using mu calculus.
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 27 January 2026