Reading an inference rule backwards to replace a desired conclusion by sufficient subgoals. A conjunction goal can be replaced by its two conjuncts using the conjunction introduction rule; an available disjunction can instead lead to two case subgoals using the disjunction elimination rule. Different choices change the organization and sharing of subproofs. Scope and assumption discharge conditions remain obligations even when a rule is applied backwards during proof search.

Ancestors (7)

  1. Natural deduction
  2. Propositional logic
  3. Mathematical logic
  4. Foundations of mathematics
  5. Area of mathematics
  6. Mathematics
  7. Home

Incoming links (1)

View article source

Discussion (0) New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version