Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction

DOI10.1007/978-3-031-09827-7_4MaRDI QIDQ6487292zbMATH OpenFDO

Authors Yutaka Nagashima

Publication date 7 December 2022

Full work available at URL https://doi.org/10.1007/978-3-031-09827-7_4

Mathematics Subject Classification ID

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

Recommendations

• Automating Induction with an SMT Solver
• scientific article; zbMATH DE number 3880144
• Extensible and efficient automation through reflective tactics
• The automation of proof by mathematical induction
• TacticToe: learning to reason with HOL4 tactics

Cites work

• A Brief Overview of HOL4
• A proof strategy language and proof script generation for Isabelle/HOL
• Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16--19, 2010. Proceedings
• Concrete semantics. With Isabelle/HOL
• Extending Sledgehammer with SMT solvers
• Goal-oriented conjecturing for Isabelle/HOL
• Hammer for Coq: automation for dependent type theory
• HOL(y)Hammer: online ATP service for HOL Light
• scientific article; zbMATH DE number 4072439 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 7649972 (Why is no real title available?)
• Induction in saturation-based proof search
• Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
• Limit-deterministic Büchi automata for linear temporal logic
• Machine Learning for Inductive Theorem Proving
• Proof-pattern recognition and lemma discovery in ACL2
• Rippling: A heuristic for guiding inductive proofs
• Superposition with structural induction
• TacticToe: learning to reason with HOL4 tactics
• The automation of proof by mathematical induction
• The Imandra Automated Reasoning System (System Description)
• The Lean theorem prover (system description)
• The Tactician. A seamless, interactive tactic learner and prover for Coq

Cited in

(2)

• Proving quantified literals in defeasible logic
• scientific article; zbMATH DE number 1301742 (Why is no real title available?)

This page was built for publication: Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction

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