Application of automated reasoning to proof translation and to finding proofs with specified properties: A case study in many-valued sentential calculus.

摘要

In both mathematics and logic, many theorems exist such that each can be proved in entirely different ways. For a striking example, there exist theorems from group theory that can be proved by relying solely on equality and (from the viewpoint of automate ...