A generic deskolemization strategy

DOI10.29007/G1TMMaRDI QIDQ7025185zbMATH OpenFDO

Authors Johann Rosain, Richard Bonichon, Julie Cailler, Olivier Hermant

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/G1TM

zbMATH Keywords

automated theorem provingfree variable tableauxproof certificateproof search proceduresskolemization

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• A compact representation of proofs
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
• Computer science -- theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3--7, 2007. Proceedings
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• scientific article; zbMATH DE number 3113496 (Why is no real title available?)
• scientific article; zbMATH DE number 3171967 (Why is no real title available?)
• scientific article; zbMATH DE number 3774914 (Why is no real title available?)
• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• scientific article; zbMATH DE number 1341475 (Why is no real title available?)
• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 1507185 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• LISA -- a modern proof system
• Logic and structure
• Mizar: state-of-the-art and beyond
• On the complexity of proof deskolemization
• On the generation of quantified lemmas
• Proving termination with multiset orderings
• The Lean theorem prover (system description)
• The liberalized -rule in free variable semantic tableaux
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Theorem Proving in Higher Order Logics
• Theorem proving modulo
• Theorem Proving via General Matings
• Towards Algorithmic Cut-Introduction
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Über eine Schlußweise aus dem Endlichen ins Unendliche.

Cited in

(1)

• Interoperability of proof systems with SC-TPTP

This page was built for publication: A generic deskolemization strategy

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