Lean induction principles for tableaux

DOI10.1007/BFB0027405MaRDI QIDQ4610315zbMATH OpenOpenAlexFDO

Authors Matthias Baaz, Uwe Egly, Christian G. Fermüller

Publication date 15 January 2019

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bfb0027405

zbMATH Keywords

automated theorem provinginduction principleinduction schemaPeano arithmeticproof search

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) First-order arithmetic and fragments (03F30)

Recommendations

• lean\(T^ AP\): Lean tableau-based deduction
• scientific article; zbMATH DE number 1552522
• scientific article; zbMATH DE number 1341483
• scientific article; zbMATH DE number 1552525
• Hyper tableaux

Cites work

• A note on semantics of logic programs with equality based on complete sets of E-unifiers
• A structure-preserving clause form translation
• Automated mathematical induction
• Equality reasoning in sequent-based calculi
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 48763 (Why is no real title available?)
• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 837782 (Why is no real title available?)
• scientific article; zbMATH DE number 227056 (Why is no real title available?)
• Mechanizing structural induction. II: Strategies
• What you always wanted to know about rigid \(E\)-unification

Cited in

(2)

• scientific article; zbMATH DE number 1341483 (Why is no real title available?)
• Non-elementary speed-ups in proof length by different variants of classical analytic calculi

This page was built for publication: Lean induction principles for tableaux

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