Proof systems for reasoning about computation errors
Studia Logica 91 (2):273 - 293 (2009)
| Abstract | In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix, incorporating both options as a non-deterministic choice. If the two strategies are to be distinguished, Kleene and McCarthy logics are combined into a logic based on a 4-valued deterministic matrix featuring two kinds of computation errors which correspond to the two computation strategies described above. For the resulting logics, we provide sound and complete calculi of ordinary, two-valued sequents. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,701 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesP. X. Monaghan (2010). A Novel Interpretation of Plato's Theory of Forms. Metaphysica 11 (1):63-78.
H. M. Malm (1989). Commodification or Compensation: A Reply to Ketchum. Hypatia 4 (3):128 - 135.
H. E. Baber (1987). How Bad Is Rape? Hypatia 2 (2):125 - 138.
C. G. Fermüller (2008). Dialogue Games for Many-Valued Logics — an Overview. Studia Logica 90 (1):43 - 68.
Katalin Bimbó (2007). $LE^{T}{Rightarrow}$ , $LR^{Circ}{Wedgesim}$ , LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557 - 570.
Analytics
Monthly downloads |
Added to index2009-03-23Total downloads4 ( #178,748 of 549,124 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
