Automated Reasoning with Analytic Tableaux and Related Methods

DOI10.1007/11554554MaRDI QIDQ5479282zbMATH OpenOpenAlexFDO

Authors Sorin Stratulat

Publication date 7 July 2006

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

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Descente Infinie + Deduction
• Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
• Sequent calculi for induction and infinite descent
• Combining induction and saturation-based theorem proving
• Inductionless induction

Cited in

(7)

• Automata-driven automated induction
• Automated Certification of Implicit Induction Proofs
• Sequent calculi for induction and infinite descent
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
• Descente Infinie + Deduction
• Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
• A unified view of induction reasoning for first-order logic

This page was built for publication: Automated Reasoning with Analytic Tableaux and Related Methods

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