The kernel of a proof assistant is one of the most important components because it represents the foundation of reasoning in that logical system. There's a lot

The kernel of a proof assistant is one of the most important components because it represents the foundation of reasoning in that logical system. There's a lot of introductory literature now, such as [0][1][2][3]. > What kind of axiomatic basis is being used in ACL2 and similar systems? ACL2 uses first-order logic and term rewriting, but this significantly hinders proof automation (done by ad-hoc searches). > Or do the different systems have significant differences with how and what they can prove? Yes. First-order logic can only quantify over individual elements of a set, second-order logic can quantify over sets, and so on. Higher-order logic is the foundation of assistants like Isabele/HOL light, which let you use classical reasoning. Alternatively (and better from an engineering standpoint) are assistants based on type theory, such as Agda, Coq and Lean. Their kernels are just type checkers, which are relatively small programs, so theorem proving in those systems is literally just functional programming with a fancy type system (though exactly how those proofs are constructed is a UX choice). > Do the systems allow explorations in reverse maths, trying to derive stuff with as little axioms as possible? Yes, in Coq you can print out the axioms (on top of the type system) that a result depends on. See [4] for information on Coq's logic and what axioms you can safely add (they are necessary for certain areas of math). [0] (Coq) https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ [1] (Agda) https://plfa.github.io/ https://plfa.github.io/ [2] (Isabelle) http://concrete-semantics.org/ http://concrete-semantics.org/ [3] (Lean) https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... [4] https://github.com/coq/coq/wiki/The-Logic-of-Coq https://github.com/coq/coq/wiki/The-Logic-of-Coq