Traditionally, mathematical logic has been content with‘in principle’formalizations of deductive inference, which place little emphasis on the description of practical reasoning. Requirements for formal descriptions of practical inference methods are now emerging however. For example, interactive reasoning systems are needed for verification of computer systems, and should support practically convenient reasoning techniques as strongly as possible. This paper describes a proof paradigm which formalises a hierarchical, problem-reduction style of reasoning which is widely useful in practical reasoning. It is a goal directed paradigm, which gives a central role to equivalence transformations. A hierarchy of subgoals can co-exist at a single point in the proof, and these subgoals may be of arbitrary type. The approach allows good access to contextual information when transforming subgoals, and can be applied to a variety of log
展开▼
