Skip to main content

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.

Filter by
Sorted by
Tagged with
15 votes
3 answers

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 ...
tinlyx's user avatar
  • 2,126
9 votes
0 answers

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 ...
march's user avatar
  • 373