Name
Abstract | ||
|---|---|---|
Soundness of inference systems for inductive proofs is sometimes shown ad hoc and a posteriori, lacking modularization and interface notions. As a consequence, these soundness proofs tend to be clumsy, difcult to understand and maintain, and error prone with difcult to localize errors. Furthermore, com- mon properties of the inference rules are often hidden, and the comparison with similar systems is difcult. To overcome these problems we propose to develop soundness proofs systematically by presenting an abstract frame inference sys- tem a priori and then to design each concrete inference rule locally as a sub-rule of some frame inference rule and to show its soundness by a small local proof establishing this sub-rule relationship. We present a frame inference system and two approaches to show its soundness, discuss an alternative, and briey clas- sify the literature. In an appendix we give an example and briey discuss failure recognition and refutational completeness. |
Year | DOI | Venue |
|---|---|---|
1994 | 10.1007/3-540-60381-6_21 | CTRS |
Keywords | Field | DocType |
inference systems,abstract notions,mathematical induction,inference rule | Disjunction introduction,Inference,Proof calculus,Algorithm,Theoretical computer science,Negation introduction,Backward chaining,Mathematical proof,Soundness,Rule of inference,Mathematics | Conference |
Volume | ISSN | ISBN |
968 | 0302-9743 | 3-540-60381-6 |
Citations | PageRank | References |
9 | 0.57 | 8 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Claus-peter Wirth | 1 | 199 | 19.22 |
| Klaus Becker | 2 | 39 | 5.54 |