Cover Image

A Higher-Order Vampire (Short Paper)

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bhayat, Ahmed, Suda, Martin
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science 68V15, 03B35, 03B16
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A new decision method for Intuitionistic Logic by 3-valued non-deterministic truth-tables (pre-print version)
by: Leme, Renato, et al.
Published: (2023)

Anatomy of a Formal Proof
by: Avigad, Jeremy, et al.
Published: (2024)

Formalizing MLTL Formula Progression in Isabelle/HOL
by: Kosaian, Katherine, et al.
Published: (2024)

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
by: Wang, Zili, et al.
Published: (2025)

Formalizing Pick's Theorem in Isabelle/HOL
by: Binder, Sage, et al.
Published: (2024)

Universal truth of operator statements via ideal membership
by: Hofstadler, Clemens, et al.
Published: (2022)

Formalising New Mathematics in Isabelle: Diagonal Ramsey
by: Paulson, Lawrence C
Published: (2025)

An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility
by: Farmer, William M.
Published: (2026)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
by: Farmer, William M., et al.
Published: (2023)

Universal Algebra in UniMath
by: Amato, Gianluca, et al.
Published: (2021)

Higher-Order Pattern Unification Modulo Similarity Relations
by: Dundua, Besik, et al.
Published: (2025)

A Modular First Formalisation of Combinatorial Design Theory
by: Edmonds, Chelsea, et al.
Published: (2021)

Single-set cubical categories and their formalisation with a proof assistant (extended version)
by: Malbos, Philippe, et al.
Published: (2024)

An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic
by: Martina, Antoine, et al.
Published: (2023)

A proof-theoretical approach to some extensions of first order quantification
by: Allègre, Loïc, et al.
Published: (2024)

The complexity of being monitorable
by: Camerlo, Riccardo, et al.
Published: (2026)

Remarks on Primitive Regulation
by: Rosko, Milan
Published: (2026)

Equivalence of finite non-deterministic logical matrices is undecidable
by: Caleiro, Carlos, et al.
Published: (2024)

ProofCloud: A Proof Retrieval Engine for Verified Proofs in Higher Order Logic
by: Wang, Shuai
Published: (2024)

Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
by: Lau, Gabriel Rongyang
Published: (2026)

Proof-theoretic methods in quantifier-free definability
by: Kocsis, Zoltan A.
Published: (2023)

Dependent Types Simplified
by: Bice, Tristan
Published: (2025)

Logical Modalities within the European AI Act: An Analysis
by: Lawniczak, Lara, et al.
Published: (2025)

LF: a Foundational Higher-Order-Logic
by: Goodsell, Zachary, et al.
Published: (2024)

Exploring P versus NP
by: Tang, Jian-Gang
Published: (2022)

Quantitative Linear Logic
by: Capucci, Matteo, et al.
Published: (2026)

A Reflection Principle for Potential Infinite Models of Type Theory
by: Eberl, Matthias
Published: (2024)

Continuous and algebraic domains in univalent foundations
by: de Jong, Tom, et al.
Published: (2024)

Weak and Strong Versions of Effective Transfinite Recursion
by: Uftring, Patrick
Published: (2022)

The Network Structure of Mathlib
by: Li, Xinze, et al.
Published: (2026)

A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem
by: Brossard, Jonathan
Published: (2026)

Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic
by: Walsh, Sean
Published: (2024)

A Minimal Substitution Basis for the Kalmár Elementary Functions
by: Prunescu, Mihai, et al.
Published: (2025)

Do not throw out the baby: Clarithmetics as alternatives to weak arithmetics
by: Japaridze, Giorgi
Published: (2026)

A propositional cirquent calculus for computability logic
by: Japaridze, Giorgi
Published: (2024)

Tao's Equational Proof Challenge Accepted (Technical Report)
by: Kondylidou, Lydia, et al.
Published: (2026)

Mechanised uniform interpolation for modal logics K, GL, and iSL
by: Férée, Hugo, et al.
Published: (2024)

Logical reduction of relations: from relational databases to Peirce's reduction thesis
by: Koshkin, Sergiy
Published: (2024)

Ordinal Analysis of Well-Ordering Principles, Well Quasi-Orders Closure Properties, and $Σ_n$-Collection Schema
by: Buriola, Gabriele, et al.
Published: (2025)

AC and the Independence of WO in Second-Order Henkin Logic, Part I
by: Gaßner, Christine
Published: (2024)