Paper Info
Title
The PCS Prover in THEOREMA
Abstract
In this paper, we present a new heuristic proving method for predicate logic, called the PCS method since it proceeds by cycling through various phases of proving (i.e. applying generic inference rules), computing (i.e. simplifying formulae), and solving (i.e. finding witness terms). Although not a complete proving calculus, it does produce very natural proofs for many propositions in elementary analysis like the limit theorems. Thus it appears to be a valuable contribution for many of the routine proofs encountered in exploring mathematical theorems.
Year
DOI
Venue
2001
10.1007/3-540-45654-6_37
EUROCAST
Keywords
Field
DocType
complete proving calculus,pcs prover,routine proof,new heuristic,natural proof,mathematical theorem,pcs method,generic inference rule,limit theorem,elementary analysis,predicate logic,inference rule
Quantifier elimination,Discrete mathematics,Computer science,Natural deduction,Theorema,Automated theorem proving,Mathematical proof,Rule of inference,Gas meter prover,Predicate logic
Conference
Volume
ISSN
ISBN
2178
0302-9743
3-540-42959-X
Citations 
PageRank 
References 
5
0.59
3
Authors
1
Name
Order
Citations
PageRank
Bruno Buchberger1847168.26