Explicitly Epistemic Contraction by Predicate Abstraction in Automated Theorem Finding: A Case Study in NBG Set Theory

摘要

In automated theorem finding by forward reasoning, there are many redundant theorems as intermediate results. This paper proposes an approach of explicitly epistemic contraction by predicate abstraction for automated theorem finding by forward reasoning in order to remove redundant theorems in a set of obtained theorems, and shows the effectiveness of the explicitly epistemic contraction by a case study of automated theorem finding in NBG set theory.