A New Application for Explanation-based Generalisation Within Automated Deduction
University of Cambridge, Computer Laboratory, 1994 - Automatic theorem proving - 18 pages
Abstract: "Generalisation is currently a major theorem-proving problem. This paper proposes a new method of generalisation, involving the use of explanation-based generalization within a new domain, which may succeed when other methods fail. The method has been implemented for simple arithmetical examples."
5 pages matching goal generalisation in this book
Results 1-3 of 5
What people are saying - Write a review
We haven't found any reviews in the usual places.
3.3 Generalisation approach appropriate cut formula arbitrary argument positions arities AUTOMATED DEDUCTION automated theorem proving Boyer & Moore constructive w-rule correct cut formula correspondence cut rule cut-free derivation described EBG method proposed EBG proof explanation-based generalisation method fail fail formalisation formula is suggested generalisation method proposed generalisation of variables generalisation tactic Generalisation using Explanation-Based goal generalisation guess h Vx Hence id-proof implementation Individual Example individual proof instances induction hypothesis induction is blocked inductive proofs instantiation linear form linear proof linearisable u>-proof linearising the w-proof method of generalisation natural deduction natural number original expression Peano Arithmetic Peano's axioms possible problem of generalisation proof environment proof of A(n proof provides provable by induction proven by induction recursive function replacing unaltered representation rewrite rule block Rules of w-Proof sequent calculus solution structure subpositions subtree successor function suitable cut formula theorem-proving type theories unaltered terms unification uniform University of Cambridge V7 len(rev(l