Barbosa, H., Fontaine, P., Reynolds, A.: Congruence closure with free variables. In: Legay, A., Margaria, T. (eds.) TACAS 2017, LNCS, vol. 10206, pp. 214–230 (2017)
Besson, F., Fontaine, P., Théry, L.: A flexible proof format for SMT: a proposal. In: Fontaine, P., Stump, A. (eds.) PxTP 2011, pp. 15–26 (2011)
Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.P., Shao, Z. (eds.) CPP 2011, LNCS, vol. 7086, pp. 135–150. Springer, Berlin (2011)
Blanchette, J.C., Böhme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reason. 56(2), 155–200 (2016)
Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 293–301. Springer, Berlin (2016)
Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L. (eds.) ITP 2010, LNCS, vol. 6172, pp. 179–194. Springer, Berlin (2010)
Barbosa, H., Blanchette, J.C., Fontaine, P.: Scalable fine-grained proofs for formula processing. In: de Moura, L. (ed.) CADE-26, LNCS. Springer, Berlin (2017)
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Technical Report, University of Iowa (2015). http://smt-lib.org/
Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18, LNCS, vol. 7180, pp. 406–419. Springer, Berlin (2012)
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)
de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Inf. Comput. 199(1–2), 24–54 (2005)
Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007, LNCS, vol. 4732, pp. 232–245. Springer, Berlin (2007)
Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 335–367. Elsevier, Amsterdam (2001)
Barrett, C., de Moura, L., Fontaine, P.: Proofs in satisfiability modulo theories. In: Woltzenlogel Paleo, B., Delahaye, D. (eds.) All About Proofs, Proofs for All, Mathematical Logic and Foundations, vol. 55, pp. 23–44. College Publications, New York (2015)
Déharbe, D., Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Exploiting symmetry in SMT problems. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE-23, LNCS, vol. 6803, pp. 222–236. Springer, Berlin (2011)
Bouton, T., de Oliveira, D.C.B., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22, LNCS, vol. 5663, pp. 151–156. Springer, Berlin (2009)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-order Logic, LNCS, vol. 2283. Springer, Berlin (2002)
Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol. 78. Springer, Berlin (1979)
Böhme, S.: Proving theorems of higher-order logic with SMT solvers. Ph.D. Thesis, Technische Universität München (2012)
Baaz, M., Egly, U., Leitsch, A.: Normal form transformations. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 273–333. Elsevier, Amsterdam (2001)
Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: Benzmüller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016, EPiC Series in Computing, vol. 41, pp. 11–23. EasyChair (2016)
Kotelnikov, E., Kovács, L., Suda, M., Voronkov, A.: A clausal normal form translation for FOOL. In: Benzmüller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016, EPiC Series in Computing, vol. 41, pp. 53–71. EasyChair (2016)
Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications, vol. 112, pp. 201–215. IOS Press, Amsterdam (2004)
Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A., (eds.) LPAR-19, LNCS, vol. 8312, pp. 735–743. Springer, Berlin (2013)
Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013, LNCS, vol. 8044, pp. 1–35. Springer, Berlin (2013). 10.1007/978-3-642-39799-8_1
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22, LNCS, vol. 5663, pp. 140–145. Springer, Berlin (2009)
de Moura, L.M., Bjørner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) LPAR 2008 Workshops, CEUR Workshop Proceedings, vol. 418. CEUR-WS.org (2008)
Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. In: LICS’87, pp. 194–204. IEEE Computer Society (1987)
Katz, G., Barrett, C.W., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Piskac, R., Talupur, M. (eds.) FMCAD 2016, pp. 93–100. IEEE Computer Society, New York (2016)
Hadarean, L., Barrett, C.W., Reynolds, A., Tinelli, C., Deters, M.: Fine grained SMT proofs for the theory of fixed-width bit-vectors. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20, LNCS, vol. 9450, pp. 340–355. Springer, Berlin (2015)
Moskal, M.: Rocket-fast proof checking for SMT solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 486–500. Springer, Berlin (2008)
Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Philos. Trans. R. Soc. Lond. Ser. A 363(1835), 2351–2375 (2005)
Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000, LNCS, vol. 1869, pp. 38–52. Springer, Berlin (2000)
Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-Pi-calculus modulo. In: Rocca, S.R.D. (ed.) TLCA 2007, LNCS, vol. 4583, pp. 102–117. Springer, Berlin (2007)
Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Log. 8(1), 1 (2007)
Graham-Lengrand, S.: Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013, LNCS, vol. 8123, pp. 149–156. Springer, Berlin (2013)
Paulson, L.C.: A higher-order implementation of rewriting. Sci. Comput. Program. 3(2), 119–149 (1983)
Meier, A.: Tramp: transformation of machine-found proofs into natural deduction proofs at the assertion level (system description). In: McAllester, D. (ed.) CADE-17, LNCS, vol. 1831, pp. 460–464. Springer, Berlin (2000)
de Nivelle, H.: Extraction of proofs from the clausal normal form transformation. In: Bradfield, J.C. (ed.) CSL 2002, LNCS, vol. 2471, pp. 584–598. Springer, Berlin (2002)
McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: a case study combining HOL-light and CVC lite. Electron. Notes Theor. Comput. Sci. 144(2), 43–51 (2006)
Fontaine, P., Marion, J.Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006, LNCS, vol. 3920, pp. 167–181. Springer, Berlin (2006)
Böhme, S., Fox, A.C.J., Sewell, T., Weber, T.: Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL. In: Jouannaud, J., Shao, Z. (eds.) CPP 2011, LNCS, vol. 7086, pp. 183–198. Springer, Berlin (2011)
Ekici, B., Katz, G., Keller, C., Mebsout, A., Reynolds, A.J., Tinelli, C.: Extending SMTCoq, a certified checker for SMT (extended abstract). In: Blanchette, J.C., Kaliszyk, C. (eds.) HaTT 2016, EPTCS, vol. 210, pp. 21–29 (2016)
Hetzl, S., Libal, T., Riener, M., Rukhaia, M.: Understanding resolution proofs through Herbrand’s theorem. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013, LNCS, vol. 8123, pp. 157–171. Springer, Berlin (2013)
Burel, G.: A shallow embedding of resolution and superposition proofs into the λΠ -calculus modulo. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, EPiC Series in Computing, vol. 14, pp. 43–57. EasyChair (2013)
Miller, D.: Proof checking and logic programming. In: Falaschi, M. (ed.) LOPSTR 2015, LNCS, vol. 9527, pp. 3–17. Springer, Berlin (2015)
