We are all familiar with calculational reasoning. A proof by calculational reasoning basically proceeds by forming a chain of intermediate results that are meant to be composed by basic principles, such as transitivity of =,<, ≤ (or similar relations).
Is the calculational style orthogonal to the Natural Deduction calculus? I mean, is it possible to compose a calculational proof using only the inference rules in Gentzen's Natural Deduction? What formal systems are usually used along with caclulational proofs? I always see calculational proofs along with axiomatic systems (not with ND). Maybe this is due to the difficulty to formalize in a calculation the introduction of hypothesis that are later discharged under certain conditions.
Can a proof using the Natural Deduction calculus be formalized in a calculational style?
What formal systems are usually used along with calculational proofs?