TY - GEN
T1 - The formal system of Dijkstra and Scholten
AU - Rocha, Camilo
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - The logic of E.W. Dijkstra and C.S. Scholten has been shown to be useful in program correctness proofs and has attracted a substantial following in research, teaching, and programming. However, there is confusion regarding this logic to the point in which, for some time, it was not considered a logic, as logicians use the word. The main objections arise from the fact that: (i) symbolic manipulations seem to be based on the meaning of the terms involved, and (ii) some notation and the proof style of the logic are different, to some extent, from those found in the traditional use of logic. This paper presents the Dijkstra-Scholten logic as a formal system, and explains its proof-theoretic foundations as a formal system, thus avoiding any confusion regarding term manipulation, notation, and proof style. The formal system is shown to be sound and complete, mainly, by using rewriting and narrowing based decision and semi-decision procedures for, respectively, propositional and first-order logic previously developed by C. Rocha and J. Meseguer.
AB - The logic of E.W. Dijkstra and C.S. Scholten has been shown to be useful in program correctness proofs and has attracted a substantial following in research, teaching, and programming. However, there is confusion regarding this logic to the point in which, for some time, it was not considered a logic, as logicians use the word. The main objections arise from the fact that: (i) symbolic manipulations seem to be based on the meaning of the terms involved, and (ii) some notation and the proof style of the logic are different, to some extent, from those found in the traditional use of logic. This paper presents the Dijkstra-Scholten logic as a formal system, and explains its proof-theoretic foundations as a formal system, thus avoiding any confusion regarding term manipulation, notation, and proof style. The formal system is shown to be sound and complete, mainly, by using rewriting and narrowing based decision and semi-decision procedures for, respectively, propositional and first-order logic previously developed by C. Rocha and J. Meseguer.
UR - http://www.scopus.com/inward/record.url?scp=84960334253&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-23165-5_27
DO - 10.1007/978-3-319-23165-5_27
M3 - Conference contribution
AN - SCOPUS:84960334253
SN - 9783319231648
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 580
EP - 597
BT - Logic, Rewriting and Concurrency - Essays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday
A2 - Ölveczky, Peter Csaba
A2 - Talcott, Carolyn
A2 - Martí-Oliet, Narciso
PB - Springer Verlag
T2 - Conference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday, 2015
Y2 - 23 September 2015 through 25 September 2015
ER -