A Higher-Order Vampire (Short Paper)

被引：0
作者：
Bhayat, Ahmed [1 ]
Suda, Martin [1 ]
机构：
[1] Czech Tech Univ, Prague, Czech Republic
来源：
AUTOMATED REASONING, IJCAR 2024, PT I | 2024年 / 14739卷
基金：
欧盟地平线“2020”;
关键词：
Vampire; Higher-Order; Strategy Scheduling;
D O I：
10.1007/978-3-031-63498-7_5
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The support for higher-order reasoning in the Vampire theorem prover has recently been completely reworked. This rework consists of new theoretical ideas, a new implementation, and a dedicated strategy schedule. The theoretical ideas are still under development, so we discuss them at a high level in this paper. We also describe the implementation of the calculus in the Vampire theorem prover, the strategy schedule construction and several empirical performance statistics.
引用
收藏
页码：75 / 85
页数：11
相关论文
共 50 条
  • [41] Recent Advances in Constructing Higher-Order DNA Structures
    Wang, Jing
    Wang, Dong-Xia
    Liu, Bo
    Jing, Xiao
    Chen, Dan-Ye
    Tang, An-Na
    Cui, Yun-Xi
    Kong, De-Ming
    CHEMISTRY-AN ASIAN JOURNAL, 2022, 17 (05)
  • [42] Higher-Order Smoothness Enhanced Graph Collaborative Filtering
    Huang, Ling
    Li, Zhi-Yuan
    He, Zhen-Yu
    Gao, Yuefang
    IEEE TRANSACTIONS ON BIG DATA, 2024, 10 (06) : 731 - 741
  • [43] Oscillation of higher-order differential equations with distributed delay
    Bazighifan, O.
    Elabbasy, E. M.
    Moaaz, O.
    JOURNAL OF INEQUALITIES AND APPLICATIONS, 2019, 2019 (1)
  • [44] Higher-order polarization singularitites in tailored vector beams
    Otte, E.
    Alpmann, C.
    Denz, C.
    JOURNAL OF OPTICS, 2016, 18 (07)
  • [45] Elliptic equations of higher-order in weighted Sobolev spaces
    Azroul E.
    Benkirane A.
    Redwane H.
    Rhoudaf M.
    Afrika Matematika, 2014, 25 (3) : 645 - 665
  • [46] On the Computation Power of Name Parameterization in Higher-order Processes
    Xu, Xian
    Yin, Qiang
    Long, Huan
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (189): : 114 - 127
  • [47] Higher-order Processes with Parameterization over Names and Processes
    Xu, Xian
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (222): : 15 - 29
  • [48] Higher-order active contour energies for gap closure
    Rochery, Marie
    Jermyn, Ian H.
    Zerubia, Josiane
    JOURNAL OF MATHEMATICAL IMAGING AND VISION, 2007, 29 (01) : 1 - 20
  • [49] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems
    Xu, Xian
    JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2009, 24 (01) : 122 - 137
  • [50] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems
    徐贤
    JournalofComputerScience&Technology, 2009, 24 (01) : 122 - 137
12345