[1] Buss, S. (1986). Bounded Arithmetic. Bibliopolis. [2] Leivant, D. (1995). Ramified recurrence and computational complexity. LICS. [3] Godefroid, P., Klarlund, N., & Sen, K. (2005). DART: Directed automated random testing. PLDI. [4] Barrett, C., & Tinelli, C. (2018). Satisfiability Modulo Theories. Handbook of Model Checking. [5] Clarke, E. et al. (2001). Bounded model checking using SMT solvers. FMCAD. [6] Coq Development Team. (2023). The Coq Proof Assistant. https://coq.inria.fr [7] Avigad, J. et al. (2020). The Lean Theorem Prover. https://leanprover.github.io [8] Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools. Addison-Wesley. [9] Truong, P. V., & Solace 52225. (2025). A Bounded Recursive Arithmetic System with Resource Guards and Termination Guarantees. Preprint.
Reader Context
Before this section, "Appendix A (omitted here) defines full evaluation rules with cost tracking" sets context for the current argument. After this page, continue to "Appendix A: Complete Operational Semantics for BSF" to follow the next step in the sequence.
This page is part of the free online edition of The Resolution of Math. Core ideas here include bounded, coq, arithmetic, model, checking. Read in sequence for full continuity, then use the related links below to compare framing across books.