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.
CITATION STYLE
Gao, H., Goto, Y., & Cheng, J. (2015). Explicitly epistemic contraction by predicate abstraction in automated theorem finding: A case study in NBG set theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9011, pp. 593–602). Springer Verlag. https://doi.org/10.1007/978-3-319-15702-3_57
Mendeley helps you to discover research relevant for your work.