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 条
  • [31] λPSI: Exact Inference for Higher-Order Probabilistic Programs
    Gehr, Timon
    Steffen, Samuel
    Vechev, Martin
    PROCEEDINGS OF THE 41ST ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '20), 2020, : 883 - 897
  • [32] Oscillation of higher-order differential equations with distributed delay
    O. Bazighifan
    E. M. Elabbasy
    O. Moaaz
    Journal of Inequalities and Applications, 2019
  • [33] Higher-order Algebras and Coalgebras from Parameterized Endofunctors
    Kim, Jiho
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2010, 264 (02) : 141 - 154
  • [34] ASYMPTOTICS FOR THE HIGHER-ORDER DERIVATIVE NONLINEAR SCHRODINGER EQUATION
    Naumkin, Pavel, I
    Sanchez-Suarez, Isahi
    COMMUNICATIONS ON PURE AND APPLIED ANALYSIS, 2021, 20 (04) : 1447 - 1478
  • [35] Superposition of Solitons with Arbitrary Parameters for Higher-order Equations
    Ankiewicz, A.
    Chowdury, A.
    ZEITSCHRIFT FUR NATURFORSCHUNG SECTION A-A JOURNAL OF PHYSICAL SCIENCES, 2016, 71 (07): : 647 - 656
  • [36] Higher-order GNN with Local Inflation for entity alignment
    Chen, Jianrui
    Yang, Luheng
    Wang, Zhihui
    Gong, Maoguo
    KNOWLEDGE-BASED SYSTEMS, 2024, 293
  • [37] A compact higher-order ADI-FDTD method
    Fu, WM
    Tan, EL
    MICROWAVE AND OPTICAL TECHNOLOGY LETTERS, 2005, 44 (03) : 273 - 275
  • [38] Higher-Order Active Contour Energies for Gap Closure
    Marie Rochery
    Ian H. Jermyn
    Josiane Zerubia
    Journal of Mathematical Imaging and Vision, 2007, 29 : 1 - 20
  • [39] Development of a higher-order ADI-FDTD method
    Wang, Z
    Chen, J
    Chen, YC
    MICROWAVE AND OPTICAL TECHNOLOGY LETTERS, 2003, 37 (01) : 8 - 12
  • [40] Stability of higher-order nonlinear impulsive differential equations
    Tang, Shuhong
    Zada, Akbar
    Faisal, Shah
    El-Sheikh, M. M. A.
    Li, Tongxing
    JOURNAL OF NONLINEAR SCIENCES AND APPLICATIONS, 2016, 9 (06): : 4713 - 4721
12345