arXiv · 2509.05653
Subsystems of Open Induction
Abstract
We study subsystems of open induction which are strongly connected to methods of automated inductive theorem proving. Specifically, we consider systems obtained from restricting induction to atoms, literals, clauses, and dual clauses. We obtain a complete picture of the relationships between these systems in the language of arithmetic and its sublanguages in terms of inclusion and strict inclusion.
Explore related subjects
Keep this discovery
Stefan Hetzl, Johannes Weiser. 2025-09-06. Subsystems of Open Induction. https://arxiv.org/abs/2509.05653
Cite the original work for its findings. Save a collection to share your selection of sources.