Skip to main content
11 votes

Proof assistants for forward reasoning?

Disclaimer: I'm a mathematician using Isabelle/ZF, with relatively little exposure to other assistants. My first experience self-learning Isabelle was similar to yours. Using ...
Pedro Sánchez Terraf's user avatar
10 votes

How to prove Gauss summation of integers with proof assistants using forward reasoning?

Like @Bubbler, I think a nice forward proof can be done using a chain of equalities, to spell out each step: ...
Joachim Breitner's user avatar
5 votes

Proof assistants for forward reasoning?

Most declarative-style provers use forward reasoning. Perhaps the most famous example is Mizar. For an introduction to Mizar, see: Mizar in a Nutshell. Some provers have a "Mizar mode" or ...
Alex Nelson's user avatar
  • 1,564
5 votes

How to prove Gauss summation of integers with proof assistants using forward reasoning?

Not exactly sure if Lean counts as "similar proof assistant" to Isabelle, but Lean mathlib has the proof of essentially the same statement, using calc mode which allows to gradually ...
Bubbler's user avatar
  • 674
4 votes

Proof assistants for forward reasoning?

The Metamath proof explorer is well-suited to forward reasoning. It has many thousands of proofs in its library, mainly based on standard ZFC set theory, presented in forward style on the website. ...
Cris P's user avatar
  • 345
1 vote
Accepted

How to apply constructor injectivity in the goal

You can write an ad-hoc tactic ...
Lolo's user avatar
  • 476

Only top scored, non community-wiki answers of a minimum length are eligible