Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Publisher: Springer
Languages: English
Types: Unknown

Classified by OpenAIRE into

This paper presents an Isabelle/HOL formalization of recent research in automated reasoning: efficient encodings of sorts in unsorted first-order logic, as implemented in Isabelle’s Sledgehammer proof tool. The formalization provides the general-purpose machinery to reason about formulas and models, emulating the theory of institutions. Quantifiers are represented using a nominal-like approach designed for interpreting syntax in semantic domains.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [1] Ballarin, C.: Locales: A module system for mathematical theories. J. Autom. Reasoning, to appear
    • [2] Berghofer, S.: First-order logic according to Fitting. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http://afp.sf.net/entries/FOL-Fitting.shtml (2007)
    • [3] Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 493-507. Springer (2013)
    • [4] Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Tech. report associated with TACAS 2013 paper [3], http://www21. in.tum.de/~blanchet/enc_types_report.pdf (2013)
    • [5] Blanchette, J.C., Krauss, A.: Monotonicity inference for higher-order formulas. J. Autom. Reasoning 47(4), 369-398 (2011)
    • [6] Blanchette, J.C., Popescu, A.: Formal development associated with this paper. http:// www21.in.tum.de/~popescua/fol_devel.zip (2013)
    • [7] Blanchette, J.C., Popescu, A., Traytel, D.: Coinductive pearl: Modular first-order logic completeness, submitted, http://www21.in.tum.de/~blanchet/compl.pdf
    • [8] Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.C.: Using first-order theorem provers in the Jahob data structure verification system. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 74-88. Springer (2007)
    • [9] Claessen, K., Lillieström, A., Smallbone, N.: Sort it out with monotonicity-Translating between many-sorted and unsorted first-order logic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE-23. LNAI, vol. 6803, pp. 207-221. Springer (2011)
    • [10] Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J. ACM 39(1), 95-146 (1992)
    • [11] Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M.C. (eds.) TPHOLs '98. LNCS, vol. 1479, pp. 153-170. Springer (1998)
    • [12] Harrison, J.: Towards self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 177-191. Springer (2006)
    • [13] Huffman, B., Urban, C.: Proof pearl: A new foundation for Nominal Isabelle. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 35-50. Springer (2010)
    • [14] Kammüller, F., Wenzel, M., Paulson, L.C.: Locales-A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs '99. LNCS, vol. 1690, pp. 149-166. Springer (1999)
    • [15] Monk, J.D.: Mathematical Logic. Springer (1976)
    • [16] Myreen, M.O., Davis, J.: A verified runtime for a verified theorem prover. In: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 265-280. Springer (2011)
    • [17] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)
    • [18] Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) IWIL-2010 (2010)
    • [19] Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Wexelblat, R.L. (ed.) PLDI '88. pp. 199-208. ACM (1988)
    • [20] Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165-193 (2003)
    • [21] Pitts, A.M.: Alpha-structural recursion and induction. J. ACM 53(3), 459-506 (2006)
    • [22] Popescu, A.: Contributions to the Theory of Syntax with Bindings and to Process Algebra. Ph.D. thesis, C.S. Dept., University of Illinois (2010)
    • [23] Popescu, A., Gunter, E.L.: Recursion principles for syntax with bindings and substitution. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP 2011. pp. 346-358. ACM (2011)
    • [24] Popescu, A., Gunter, E.L., Osborn, C.J.: Strong normalization of System F by HOAS on top of FOAS. In: LICS 2010. pp. 31-40. IEEE (2010)
    • [25] Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T.F. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 294-309. Springer (2005)
    • [26] Shankar, N.: Metamathematics, Machines, and Gödel's Proof, Cambridge Tracts in Theoretical Computer Science, vol. 38. Cambridge University Press (1994)
    • [27] Sutcliffe, G.: The 6th IJCAR automated theorem proving system competition-CASC-J6. AI Comm. 26(2), 211-223 (2013)
    • [28] Tinelli, C., Zarba, C.: Combining decision procedures for sorted theories. In: Alferes, J., Leite, J. (eds.) JELIA 2004. LNCS, vol. 3229, pp. 641-653. Springer (2004)
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article