Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar

Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar

1980

Earlier work this paper cites.

Pons, O., Bertot, Y., Rideau, L.: Notions of dependency in proof assistants. In: UITP 1998. Eindhoven University of Technology (1998)

1998

Earlier work this paper cites.

Bertot, Y., Pons, O., Pottier, L.: Dependency graphs for interactive theorem provers. Tech. rep., INRIA (2000), report RR-4052

2000

Earlier work this paper cites.

Asperti, A., Padovani, L., Coen, C.S., Guidi, F., Schena, I.: Mathematical knowledge management in HELM. Ann. Math. Artif. Intell. 38(1-3), 27–46 (2003)

2003

Earlier work this paper cites.

Matuszewski, R., Rudnicki, P.: Mizar

2005

Earlier work this paper cites.

Haftmann, F., Wenzel, M.: Constructive type classes in isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES. Lecture Notes in Computer Science, vol. 4502, pp. 160–174. Springer (2006)

2006

Earlier work this paper cites.

Urban, J.: MoMM—fast interreduction and retrieval in large libraries of formalized mathematics. International Journal on Artificial Intelligence Tools 15(1), 109–130 (2006)

2006

Cited alongside, same era.

Mamane, L., Geuvers, H.: A document-oriented Coq

2007

Cited alongside, same era.

Wiedijk, F.: Mizar’s soft type system. In: Schneider, K., Brandt, J. (eds.) TPHOLs. Lecture Notes in Computer Science, vol. 4732, pp. 383–399. Springer (2007)

2007

Cited alongside, same era.

Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Tobias Nipkow, Christian Urban (eds.) TPHOLs. LNCS, vol. 5674. Springer (2009), http://hal.inria.fr/inria-00368403/en/

2009

Cited alongside, same era.

Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7(1), 41–57 (2009)

2009

Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar

2010

Later among the works it cites.

Alama, J., Kühlwein, D., Tsivtsivadze, E., Urban, J., Heskes, T.: Premise selection for mathematics by corpus analysis and kernel methods. CoRR abs/1108.3446 (2011), http://arxiv.org/abs/1108.3446

Original

2011

Closest in time.

Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: CADE 11 (2011), to appear

2011

Closest in time.

Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. CoRR abs/1102.1323 (2011)

Original

2011

Closest in time.

Alama, J., Kuehlwein, D., Urban, J.: Automated and human proofs in general mathematics: An initial comparison. In: LPAR. Lecture Notes in Computer Science, Springer (2012), accepted

2012