Exploiting instantiations from paramodulation proofs in Isabelle/HOL

DOI10.1007/978-3-031-99984-0_30MaRDI QIDQ6869927zbMATH OpenFDO

Authors Lukas Bartl, Jasmin Christian Blanchette, Tobias Nipkow

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_30

zbMATH Keywords

instantiationsIsabelle/HOLparamodulationsledgehammer

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A formalization and proof checker for Isabelle's metalogic
• A higher-order Vampire (short paper)
• A learning-based fact selector for Isabelle/HOL
• A new implementation technique for applicative languages
• A semantic framework for proof evidence
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Encoding monomorphic and polymorphic types
• Equational reasoning in Isabelle
• Extending a high-performance prover to higher-order logic
• From rewrite rules to axioms in the \(\lambda \varPi \)-calculus modulo theory
• scientific article; zbMATH DE number 1543300 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Lightweight relevance filtering for machine-generated resolution problems
• Making higher-order superposition work
• Mining the Archive of Formal Proofs
• More SPASS with Isabelle
• On restrictions of ordered paramodulation with simplification
• Semi-intelligible Isar proofs from machine-generated proofs
• Seventeen provers under the hammer
• Sledgehammer: judgement day
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• System description: GAPT 2.0
• The higher-order prover Leo-III
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee
• Tools and algorithms for the construction and analysis of systems. 28th international conference, TACAS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2--7, 2022. Proceedings. Pa
• Translating higher-order clauses to first-order clauses
• Type Reconstruction for Type Classes

This page was built for publication: Exploiting instantiations from paramodulation proofs in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869927)