Finding new theorems is essential for the general progress in mathematics, Apart from creating and proving completely new theorems progress can also be achieved by theorem reuse; i.e, by translating theorems from related theories into the target theory and proving its translated premises under which the theorem was proven. This approach is pursued by the "little theories" and the development graph paradigms. This work suggests an improvement in this direction in two aspects; partial theory inclusions enhances theorem reuse and formula matching to support automated detection of theory inclusions. By representing theory axioms as facts and partial theories (i.e. theorems and their minimal set of premises) as horn clauses, reusable theorems correspond to derived facts such that model generator like KRHyper can be used for this task. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Normann, I. (2006). Enhanced theorem reuse by partial theory inclusions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4120 LNAI, pp. 40–52). Springer Verlag. https://doi.org/10.1007/11856290_6
Mendeley helps you to discover research relevant for your work.