Name
Abstract | ||
|---|---|---|
A major barrier to more common use of mechanical theorem provers in verifying software designs is the significant distance between proof styles natural to humans and proof styles supported by mechanical provers. To make mechanical provers useful to software designers with some mathematical sophistication but without expertise in mechanical provers, the distance between hand proofs and their mechanized versions must be reduced. To achieve this, we are developing a mechanical prover called TAME... |
Year | DOI | Venue |
|---|---|---|
1997 | 10.1007/BFb0028384 | TPHOLs |
Keywords | Field | DocType |
human-style theorem proving,feedback,theorems,software design,verification,theorem prover,automata,theorem proving | Computer-assisted proof,Programming language,Computer science,Theoretical computer science,Natural proof,Gas meter prover,Distributed computing,Specification language,Discrete mathematics,Automated theorem proving,Automaton,Algorithm,Mathematical proof,Proof assistant | Conference |
ISBN | Citations | PageRank |
3-540-63379-0 | 12 | 0.94 |
References | Authors | |
14 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Myla Archer | 1 | 463 | 56.43 |
| Constance L. Heitmeyer | 2 | 898 | 151.71 |