Calculational Proofs
July 2022
Pages 231 - 246
References
[1]
R. Back and J. von Wright. 1998. Refinement Calculus—A Systematic Introduction. Graduate Texts in Computer Science. Springer.
[2]
R. Backhouse. 2003. Program Construction—Calculating Implementations from Specifications. John Wiley.
[3]
L. Bijlsma and R. Nederpelt. 1998. Dijkstra–Scholten predicate calculus: Concepts and misconceptions. Acta Inf. 35, 12, 1007–1036.
[4]
E. Börger. 1994. Book review: E.W. Dijkstra, C.S. Scholten, Predicate Calculus and Program Semantics. Sci. Comput. Program. 23, 91–101.
[5]
Edsger W. Dijkstra and Carel S. Scholten. 1990. Predicate Calculus and Program Semantics. Springer-Verlag.
[6]
E. W. Dijkstra and J. Misra. 2001. Designing a calculational proof of Cantor’s theorem. Am. Math. Mon. 108, 5, 440–443.
[7]
R. M. Dijkstra. 1996. “Everywhere” in predicate algebra and modal logic. Inf. Process. Lett. 58, 5, 237–243.
[8]
P. Ferraris, J. Lee, and V. Lifschitz. 2011. Stable models and circumscription. Artif. Intell. 175, 1, 236–263.
[9]
J. Garson. 2021. Modal logic. In E. N. Zalta (Ed.), The Stanford Encyclopedia of Philosophy (Summer 2021 Edition). Stanford University. https://plato.stanford.edu/entries/logic-modal/.
[10]
G. K. E. Gentzen. 1934. Untersuchungen über das logische Schließen. I. Math. Z. 39, 176–210.
[11]
D. Gries and F. Schneider. 1993. A Logical Approach to Discrete Math. Springer.
[12]
D. Gries and F. Schneider. 1995. Equational propositional logic. Inf. Process. Lett. 53, 3, 145–152.
[13]
D. Gries and F. Schneider. 1998. Adding the everywhere operator to propositional logic. J. Log. Comput. 8, 1, 119–129.
[14]
A. Kaldewaij. 1990. Programming—The Derivation of Algorithms. Prentice Hall International Series in Computer Science. Prentice Hall.
[15]
V. Lifschitz. 2002. On calculational proofs. Ann. Pure Appl. Log. 113, 207–224.
Index Terms
- Calculational Proofs
Index terms have been assigned to the content through auto-classification.
Recommendations
From proofs to focused proofs: a modular proof of focalization in linear logic
CSL'07/EACSL'07: Proceedings of the 21st international conference, and Proceedings of the 16th annuall conference on Computer Science LogicProbably the most significant result concerning cut-free sequent calculus proofs in linear logic is the completeness of focused proofs. This completeness theorem has a number of proof theoretic applications -- e.g. in game semantics, Ludics, and proof ...
Referential logic of proofs
Clifford lectures and the mathematical foundations of programming semanticsWe introduce an extension of the propositional logic of single-conclusion proofs by the second-order variables denoting the reference constructors of the type "the formula which is proved by x." The resulting Logic of Proofs with References, FLPref, is ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 13 July 2022
Check for updates
Qualifiers
- Chapter
Appears in
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 1Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in