Paper Info
Title
Inductive Theorem Proving by Consistency for First-Order Clauses
Abstract
We show how the method of proof by consistency can be extended to proving properties of the perfect model of a set of first-order clauses with equality. Technically proofs by consistency will be similar to proofs by case analysis over the term structure. As our method also allows to prove sufficient-completeness of function definitions in parallel with proving an inductive theorem we need not distinguish between constructors and defined functions. Our method is linear and refutationally complete with respect to the perfect model, it supports lemmas in a natural way, and it provides for powerful simplification and elimination techniques.
Year
DOI
Venue
1992
10.1007/3-540-56393-8_17
CTRS
Keywords
Field
DocType
inductive theorem proving,first-order clauses,first order,term structure,theorem proving
Inductive theorem proving,Discrete mathematics,Horn clause,First order,Mathematical proof,Unit propagation,Calculus,Lemma (mathematics),Mathematics,Case analysis
Conference
ISBN
Citations 
PageRank 
3-540-56393-8
15
0.90
References 
Authors
16
2
Name
Order
Citations
PageRank
Harald Ganzinger11513155.21
Jürgen Stuber2847.16