Skip to main content

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.

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 goal is proved if all subgoals (and their sub-subgoals) are proved. Backward proofs are widely used in proof assistants such as Isabelle, Coq among many others.