Questions tagged [backward-proof]
Backward proofs are a type of proofs and logical reasoning that start from the goal and then use a set of inference rules backwards to obtain a set of sub-goals. The end goal is proved if all its subgoals (and their sub-subgoals etc.) are proved. Use this tag for proofs or reasoning processing in the backward direction.
3
questions
8
votes
2
answers
143
views
How to prove Gauss summation of integers with proof assistants using forward reasoning?
As shown in an exercise here, we can prove the Gauss summation (that $\Sigma_{i=0..n}{i} = n \cdot (n + 1)/2$ ) in Isabelle/Isar using mathematical induction, as follows.
...
- 1,506
8
votes
0
answers
109
views
Has there been any work on automated translation of tactic proofs to everyday language?
There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could ...
- 363
15
votes
3
answers
249
views
Proof assistants for forward reasoning?
I have only very limited learning experience with Isabelle and Coq. An issue while learning to use proof assistants is that forward proof is cumbersome or difficult. For example, the first time I saw ...
- 1,506