Fetching the paper…
Reading the bibliography…
Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development.
Tarski, A.: On well-ordered subsets of any set. Fundamenta Mathematicae 32, 176–183 (1939)
1939
Earlier work this paper cites.
Aronszajn, N.: Theory of reproducing kernels. Transactions of the American Mathematical Society 68 (1950)
1950
Earlier work this paper cites.
Davis, M.: Obvious logical inferences. In: Hayes, P.J. (ed.) IJCAI. pp. 530–531. William Kaufmann (1981)
1981
Earlier work this paper cites.
Rudnicki, P.: Obvious inferences. J. Autom. Reasoning 3(4), 383–393 (1987)
1987
Earlier work this paper cites.
Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE. Lecture Notes in Computer Science, vol. 1104, pp. 313–327. Springer (1996)
1996
Earlier work this paper cites.
Brin, S., Page, L.: The anatomy of a large-scale hypertextual web search engine. Computer Networks 30(1-7), 107–117 (1998)
1998
Earlier work this paper cites.
Carlson, A., Cumby, C., Rizzolo, N., Rosen, J., Roth, D.: SNoW user manual (1999), http://l2r.cs.uiuc.edu/~cogcomp/software/snow-userguide.pdf
1999
Earlier work this paper cites.
Schoelkopf, B., Herbrich, R., Williamson, R., Smola, A.J.: A Generalized Representer Theorem. In: Helmbold, D., Williamson, R. (eds.) Proceedings of the 14th Annual Conference on Computational Learning Theory. pp. 416–426. Berlin, Germany (2001)
2001
Earlier work this paper cites.
Scholkopf, B., Smola, A.J.: Learning with Kernels: Support Vector Machines, Regularization, Optimization, and Beyond. MIT Press, Cambridge, MA, USA (2001)
2001
Earlier work this paper cites.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283. Springer (2002)
2002
Earlier work this paper cites.
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91–110 (2002)
2002
Earlier work this paper cites.
Rifkin, R., Yeo, G., Poggio, T., Rifkin, R., Yeo, G., Poggio, T.: Regularized Least-Squares Classification. In: Suykens, J., Horvath, G., Basu, S., Micchelli, C., Vandewalle, J. (eds.) Advances in Learning Theory: Methods, Model and Applications NATO Science Series III: Computer and Systems Sciences, vol. 190, pp. 131–154. IOS Press (2003)
2003
Earlier work this paper cites.
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, Springer Verlag (2004)
2004
Earlier work this paper cites.
Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, New York, NY, USA (2004)
2004
Cited alongside, same era.
Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications 4, 3–24 (2005)
2005
Cited alongside, same era.
Harrison, J., Slind, K., Arthan, R.: HOL. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. Lecture Notes in Computer Science, vol. 3600, pp. 11–19. Springer (2006)
2006
Cited alongside, same era.
Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning 37(1-2), 21–43 (2006)
2006
Cited alongside, same era.
Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs. Lecture Notes in Computer Science, vol. 4732, pp. 232–245. Springer (2007)
Richard, M.D., Lippmann, R.P.: Neural Network Classifiers Estimate Bayesian a posteriori Probabilities. Neural Computation 3(4), 461–483 (2010)
2010
Later among the works it cites.
Tsivtsivadze, E., Pahikkala, T., Boberg, J., Salakoski, T., Heskes, T.: Co-regularized least-squares for label ranking. In: Hüllermeier, E., Fürnkranz, J. (eds.) Chapter in Preference Learning Book). pp. 107–123 (2010)
2010
Later among the works it cites.
Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar mathematical library. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS. Lecture Notes in Computer Science, vol. 6327, pp. 155–166. Springer (2010)
2010
Later among the works it cites.
Urban, J., Sutcliffe, G.: Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC/MKM/Calculemus. Lecture Notes in Computer Science, vol. 6167, pp. 132–146. Springer (2010)
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
2007
Cited alongside, same era.
Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.) ESARLT. CEUR Workshop Proceedings, vol. 257. CEUR-WS.org (2007)
2007
Cited alongside, same era.
Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35–60 (2008)
2008
Cited alongside, same era.
Solovay, R.: AC and strongly inaccessible cardinals. Available on the Foundations of Mathematics archives at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html (March 29 2008)
2008
Cited alongside, same era.
Urban, J., Sutcliffe, G., Pudlák, P., Vyskocil, J.: MaLARea SG1–machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR. Lecture Notes in Computer Science, vol. 5195, pp. 441–456. Springer (2008)
2008
Cited alongside, same era.
Alama, J.: Formal Proofs and Refutations. Ph.D. thesis, Stanford University (2009)
2009
Cited alongside, same era.
Simpson, S.G.: Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic, Springer, 2 edn. (2009)
2009
Cited alongside, same era.
Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. Journal of Formalized Reasoning 3(2), 153–245 (2010)
2010
Cited alongside, same era.
2010
Later among the works it cites.
Alama, J., Brink, K., Mamane, L., Urban, J.: Large formal wikis: Issues and solutions. In: Davenport, J., Farmer, W., Urban, J., Rabe, F. (eds.) Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 6824, pp. 133–148. Springer Berlin / Heidelberg (2011)
2011
Closest in time.
2011
Closest in time.
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos. Lecture Notes in Computer Science, vol. 6989, pp. 12–27. Springer (2011)
2011
Closest in time.
Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction – CADE-23, Lecture Notes in Computer Science, vol. 6803, pp. 299–314. Springer Berlin / Heidelberg (2011)
2011
Closest in time.
Shalev-Shwartz, S., Singer, Y., Srebro, N., Cotter, A.: Pegasos: primal estimated sub-gradient solver for SVM. Math. Program. 127(1), 3–30 (2011)
2011
Closest in time.
2011
Closest in time.
Urban, J., Vyskocil, J., Stepánek, P.: MaLeCoP: Machine learning connection prover. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX. Lecture Notes in Computer Science, vol. 6793, pp. 263–277. Springer (2011)
2011
Closest in time.
Alama, J., Kühlwein, D., Urban, J.: Automated and human proofs in general mathematics: An initial comparison. In: Bjørner, N., Voronkov, A. (eds.) LPAR. Lecture Notes in Computer Science, vol. 7180, pp. 37–45. Springer (2012)
2012
Closest in time.