UTCS Artificial Intelligence
courses
talks/events
demos
people
projects
publications
software/data
labs
areas
admin
Vladimir Lifschitz
This note is about the "calculational style" of presenting proofs introduced by Dijkstra and Scholten and adopted in some books on theoretical computer science. We define the concept of a calculation, which is a formal counterpart of the idea of a calculational proof. The definition is in terms of a new formalization DS of predicate logic. Any proof tree in the system DS can be represented as a sequence of calculations. This fact shows that any logically valid predicate formula has a calculational proof.
View:
PS
Citation:
Annals of Pure and Applied Logic
, Vol. 113 (2002), pp. 207-224.
Bibtex:
@article{lif01b, title={On Calculational Proofs}, author={Vladimir Lifschitz}, volume={113}, journal={Annals of Pure and Applied Logic}, pages={207-224}, url="http://www.cs.utexas.edu/users/ai-lab/?lif01b", year={2002} }
People
Vladimir Lifschitz
Faculty
vl [at] cs utexas edu
Areas of Interest
Logic
Labs
Texas Action Group