A new application for explanation-based generalisation within automated deduction

DOI10.1007/3-540-58156-1_13zbMath1433.68529OpenAlexW1482833009MaRDI QIDQ5210770

No author found.

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_13

Mathematics Subject Classification ID

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

Uses Software

• HOL

Cites Work

• A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure
• Proof theory. 2nd ed
• Transfinite recursive progressions of axiomatic theories
• Gödel Theorems for Non-Constructive Logics
• On the interpretation of non-finitist proofs–Part II
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A new application for explanation-based generalisation within automated deduction