Pgeon: generating tableau-based provers from declarative specifications of logical calculi

DOI10.1007/978-3-032-32589-1_6MaRDI QIDQ7411157zbMATH OpenFDO

Authors Romain Sidhoum, Simon Robillard, David Delahaye

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32589-1_6

zbMATH Keywords

automated prover generationlogical frameworktableau calculi

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A tactic language for the system Coq
• Contraction-free sequent calculi for intuitionistic logic
• scientific article; zbMATH DE number 2177623 (Why is no real title available?)
• IeanCOP: lean connection-based theorem proving
• lean\(T^ AP\): Lean tableau-based deduction
• Lotrec: The generic tableau prover for modal and description logics
• Sequoia: A Playground for Logicians
• The Tableau Workbench

This page was built for publication: Pgeon: generating tableau-based provers from declarative specifications of logical calculi

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