Cover Image

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bartl, Lukas, Blanchette, Jasmin, Nipkow, Tobias
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Brownian Motion in Isabelle/HOL
by: Laursen, Christian Pardillo, et al.
Published: (2024)

Linear Programming in Isabelle/HOL
by: Parsert, Julian
Published: (2024)

Verifying Numerical Methods with Isabelle/HOL
by: Bryant, Dustin, et al.
Published: (2025)

Complex Bounded Operators in Isabelle/HOL
by: Unruh, Dominique, et al.
Published: (2025)

Stalnaker's Epistemic Logic in Isabelle/HOL
by: Guzman, Laura P. Gamboa, et al.
Published: (2024)

Formalization of Differential Privacy in Isabelle/HOL
by: Sato, Tetsuya, et al.
Published: (2024)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
by: Foster, Simon, et al.
Published: (2024)

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
by: Binder, Sage, et al.
Published: (2026)

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
by: Hulak, David B., et al.
Published: (2026)

Munkres' General Topology Autoformalized in Isabelle/HOL
by: Bryant, Dustin, et al.
Published: (2026)

Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
by: Munive, Jonathan Julián Huerta y, et al.
Published: (2024)

Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL
by: Kim, Jinwook
Published: (2026)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
by: Stübinger, Terru, et al.
Published: (2023)

A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL
by: Schmoetten, Richard, et al.
Published: (2024)

SAT-Inspired Higher-Order Eliminations
by: Blanchette, Jasmin, et al.
Published: (2022)

L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
by: Linzi, Alessandro
Published: (2025)

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

Proof Recommendation System for the HOL4 Theorem Prover
by: Dekhil, Nour, et al.
Published: (2024)

Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library
by: Bilotta, Antonella
Published: (2025)

From MBQI to Enumerative Instantiation and Back
by: Dančo, Marek, et al.
Published: (2025)

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

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

Quantifier Instantiations: To Mimic or To Revolt?
by: Jakubův, Jan, et al.
Published: (2025)

Term Orders for Optimistic Lambda-Superposition
by: Bentkamp, Alexander, et al.
Published: (2025)

Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds
by: Huch, Fabian
Published: (2024)

Fault-Tolerant Multiparty Session Types with Global Escape Loops
by: Bartl, Lukas, et al.
Published: (2025)

Proofs that Modify Proofs, 1/2
by: Towsner, Henry
Published: (2025)

Optimistic Higher-Order Superposition
by: Bentkamp, Alexander, et al.
Published: (2025)

Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security
by: Kammüller, Florian
Published: (2023)

A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version)
by: Ge, Rui, et al.
Published: (2024)

Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
by: Stevens, Lukas, et al.
Published: (2025)

The Unification Type of an Equational Theory May Depend on the Instantiation Preorder: From Results for Single Theories to Results for Classes of Theories
by: Baader, Franz, et al.
Published: (2026)

The Proof Analysis Problem
by: Arteche, Noel, et al.
Published: (2025)

Mechanized HOL Reasoning in Set Theory
by: Guilloud, Simon, et al.
Published: (2024)

Proof-theoretic Semantics for Second-order Logic
by: Gheorghiu, Alexander V., et al.
Published: (2025)

Proof-theoretic Semantics for the Logic of Bunched Implications
by: Gu, Tao, et al.
Published: (2023)

Proof-theoretic Semantics for First-order Logic
by: Gheorghiu, Alexander V.
Published: (2024)

Cyclic Proofs for iGL via Corecursion
by: Miranda, Borja Sierra
Published: (2023)

Proof Complexity of Linear Logics
by: Tabatabai, Amirhossein Akbar, et al.
Published: (2026)

Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model
by: Kappelmann, Kevin, et al.
Published: (2025)