Verified path indexing

DOI10.1007/978-3-031-99984-0_14MaRDI QIDQ6869951zbMATH OpenFDO

Authors Mohamed Chaabani, Simon Robillard

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_14

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 verified SAT solver framework with learn, forget, restart, and incrementality
• Automatic Data Refinement
• Concrete semantics. With Isabelle/HOL
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Term indexing

This page was built for publication: Verified path indexing

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