4 ms·

I find semi-automaticed theorem proving a very interesting field, because I'm fascinated by axiomatic systems and the fundamentals of logic and maths, but I don

I find semi-automaticed theorem proving a very interesting field, because I'm fascinated by axiomatic systems and the fundamentals of logic and maths, but I don't have any experience of using them, yet. What kind of axiomatic basis is being used in ACL2 and similar systems? Is the basics just modus ponens and the axioms are provided as a library? Or do the different systems have significant differences with how and what they can prove? Do the systems allow explorations in reverse maths, trying to derive stuff with as little axioms as possible?

siraben 5y ago
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
plafl 5y ago
If you want a gentle introduction you may like this book http://the-little-prover.github.io/ http://the-little-prover.github.io/
voxl 5y ago
Any dependent type theory is "semi-automated" because judgemental equality computes normal forms, there is no reason it should be this way, other than convenience of course.

siraben 5y ago

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

plafl 5y ago

If you want a gentle introduction you may like this book http://the-little-prover.github.io/ http://the-little-prover.github.io/

voxl 5y ago

Any dependent type theory is "semi-automated" because judgemental equality computes normal forms, there is no reason it should be this way, other than convenience of course.