Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H. TPS: A theorem-proving system for classical type theory. J. Autom. Reason. 16, 3 (1996), 321--353.

Crossref

Google Scholar

[2]

Bachmair, L., Ganzinger, H. Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4, 3 (1994), 217--247.

Crossref

Google Scholar

[3]

Bachmair, L., Ganzinger, H. Resolution theorem proving. In Handbook of Automated Reasoning, Vol. I, J.A. Robinson and A. Voronkov, eds. (2001). Elsevier and MIT Press, 19--99.

Crossref

Google Scholar

[4]

Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W. Extending SMT solvers to higher-order logic. In CADE-27 (LNCS, Vol. 11716), P. Fontaine, ed., (2019). Springer, 35--54.

Google Scholar

[5]

Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P. Superposition for full higher-order logic. In CADE-28 (LNCS, Vol. 12699), A. Platzer, G. Sutcliffe, eds. (2021). Springer, 396--412.

Google Scholar

[6]

Benzmüller, C., Kohlhase, M. Extensional higher-order resolution. In CADE-15 (LNCS, Vol. 1421), C. Kirchner, H. Kirchner, eds. (1998). Springer, 56--71.

Google Scholar

[7]

Benzmüller, C., Sultana, N., Paulson, L.C., Theiss, F. The higher-order prover LEO-II. J. Autom. Reason. 55, 4 (2015), 389--404.

Digital Library

Google Scholar

[8]

Bhayat, A., Reger, G. A combinator-based superposition calculus for higher-order logic. In IJCAR 2020, Part I (LNCS, Vol. 12166), N. Peltier, V. Sofronie-Stokkermans, eds. (2020). Springer, 278--296.

Digital Library

Google Scholar

[9]

Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J. Hammering towards QED. J. Formaliz. Reason. 9, 1 (2016), 101--148.

Google Scholar

[10]

Brown, C.E. Satallax: An automatic higher-order prover. In IJCAR 2012 (LNCS, Vol. 7364), B. Gramlich, D. Miller, U. Sattler, eds. (2012). Springer, 111--117.

Google Scholar

[11]

Church, A. A note on the Entscheidungsproblem. J. Symb. Logic 1, 1 (1936), 40--41.

Google Scholar

[12]

Desharnais, M., Vukmirović, P., Blanchette, J., Wenzel, M. Seventeen provers under the hammer. In ITP 2022 (LIPIcs, Vol. 237), J. Andronick, L. de Moura, eds. (2022). Schloss Dagstuhl---Leibniz-Zentrum für Informatik, 8:1--8:18.

Google Scholar

[13]

Gödel, K. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38, 1 (1931), 173--198.

Google Scholar

[14]

Huet, G.P. A mechanization of type theory. In IJCAI-73, N.J. Nilsson, ed. (1973). William Kaufmann, 139--146.

Google Scholar

[15]

Huet, G.P. The undecidability of unification in third order logic. Inf. Control. 22, 3 (1973), 257--267.

Crossref

Google Scholar

[16]

Huet, G.P. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1, 1 (1975), 27--57.

Crossref

Google Scholar

[17]

Lindblad, F. A focused sequent calculus for higher-order logic. In IJCAR 2014 (LNCS, Vol. 8562), S. Demri, D. Kapur, C. Weidenbach, eds. (2014). Springer, 61--75.

Google Scholar

[18]

Lucchesi, C.L. The undecidability of the unification problem for third order languages. Report CSRR 2059 (1972), 129--198.

Google Scholar

[19]

Malik, S., Zhang, L. Boolean satisfiability: From theoretical hardness to practical success. Commun. ACM 52, 8 (2009), 76--82.

Digital Library

Google Scholar

[20]

Pietrzykowski, T. A complete mechanization of second-order type theory. JACM 20, 2 (1973), 333--364.

Digital Library

Google Scholar

[21]

Plotkin, G. Building-in equational theories. Mach. Intell. 7 (1972), 73--90.

Google Scholar

[22]

Robinson, J.A. A machine-oriented logic based on the resolution principle. J. ACM 12, 1 (1965), 23--41.

Digital Library

Google Scholar

[23]

Schulz, S., Cruanes, S., Vukmirović, P. Faster, higher, stronger: E 2.3. In CADE-27 (LNCS, Vol. 11716), P. Fontaine, ed. (2019). Springer, 495--507.

Google Scholar

[24]

Steen, A., Benzmüller, C. The higher-order prover Leo-III. In IJCAR 2018 (LNCS, Vol. 10900), D. Galmiche, S. Schulz, R. Sebastiani, eds. (2018). Springer, 108--116.

Google Scholar

[25]

Stroustrup, B. The Design and Evolution of C++. Addison-Wesley, 1995.

Digital Library

Google Scholar

[26]

Sultana, N., Blanchette, J.C., Paulson, L.C. LEO-II and Satallax on the Sledgehammer test bench. J. Appl. Logic 11, 1 (2013), 91--102.

Crossref

Google Scholar

[27]

Sutcliffe, G. The CADE ATP System Competition---CASC. AI Mag. 37, 2 (2016), 99--101.

Google Scholar

[28]

Sutcliffe, G., Desharnais, M. The CADE-28 Automated Theorem Proving System Competition---CASC-28. AI Commun. 34, 4 (2022), 259--276.

Digital Library

Google Scholar

[29]

Turing, A.M. On computable numbers, with an application to the Entscheidungsproblem. Proc. London Math. Soc. s2-42, 1 (1937), 230--265.

Crossref

Google Scholar

[30]

Vukmirović;, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S. Making higher-order superposition work. In CADE-28 (LNCS, Vol. 12699), A. Platzer, G. Sutcliffe, eds. (2021). Springer, 415--432.

Google Scholar

[31]

Vukmirović, P., Blanchette, J., Cruanes, S., Schulz, S. Extending a brainiac prover to lambda-free higher-order logic. Int. J. Softw. Tools Technol. Transf. 24, 1 (2022), 67--87.

Digital Library

Google Scholar

Cited By

View all

Lund SVilladsen J(2024)Teaching Higher-Order Logic Using IsabelleElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.400.5400(59-78)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.400.5
Kœhler TGoens ABhat SGrosser TTrinder PSteuwer M(2024)Guided Equality SaturationProceedings of the ACM on Programming Languages10.1145/36329008:POPL(1727-1758)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632900
Steen ABenzmüller C(2024)Challenges for Non-Classical Reasoning in Contemporary AI ApplicationsKI - Künstliche Intelligenz10.1007/s13218-024-00855-8Online publication date: 4-Jul-2024
https://doi.org/10.1007/s13218-024-00855-8
Show More Cited By

Index Terms

Mechanical Mathematicians

Recommendations

Advances in Mechanical Engineering: Selected Contributions from the Conference Modern Engineering Science and Education, Saint Petersburg, Russia
Advances in Mechanical Engineering: Selected Contributions from the Conference Modern Engineering Science and Education, Saint Petersburg, Russia, ...
Formal Mathematics for Mathematicians

The collection of works for this special issue was inspired by the presentations given at the 2011 AMS Special Session on Formal Mathematics for Mathematicians: Developing Large Repositories of Advanced Mathematics. The issue features a collection of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Communications of the ACM Volume 66, Issue 4

April 2023

94 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/3589208

Editor:
James Larus
Association for Computing Machinery, New York, NY

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 March 2023

Published in CACM Volume 66, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Funding Sources

European Research Council
Chinese Academy of Sciences President?s International Fellowship for Postdoctoral Researchers
Netherlands Organization for Scientific Research
Natural Science Foundation of China

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
2,246
Total Downloads

Downloads (Last 12 months)1,554
Downloads (Last 6 weeks)304

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Lund SVilladsen J(2024)Teaching Higher-Order Logic Using IsabelleElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.400.5400(59-78)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.400.5
Kœhler TGoens ABhat SGrosser TTrinder PSteuwer M(2024)Guided Equality SaturationProceedings of the ACM on Programming Languages10.1145/36329008:POPL(1727-1758)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632900
Steen ABenzmüller C(2024)Challenges for Non-Classical Reasoning in Contemporary AI ApplicationsKI - Künstliche Intelligenz10.1007/s13218-024-00855-8Online publication date: 4-Jul-2024
https://doi.org/10.1007/s13218-024-00855-8
Avigad J(2024)Automated Reasoning for MathematicsAutomated Reasoning10.1007/978-3-031-63498-7_1(3-20)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_1
Bentkamp ABlanchette JNummelin VTourret SWaldmann U(2023)Complete and Efficient Higher-Order Reasoning via Lambda-SuperpositionACM SIGLOG News10.1145/3636362.363636710:4(25-40)Online publication date: 4-Dec-2023
https://dl.acm.org/doi/10.1145/3636362.3636367

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Digital Edition

View this article in digital edition.

Digital Edition

Magazine Site

View this article on the magazine site (external)

Magazine Site

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

Advances in Mechanical Engineering: Selected Contributions from the Conference Modern Engineering Science and Education, Saint Petersburg, Russia

Advances in Mechanical Engineering: Selected Contributions from the Conference Modern Engineering Science and Education, Saint Petersburg, Russia, ...

Formal Mathematics for Mathematicians

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Funding Sources

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Digital Edition

Magazine Site

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations