Interpreting modal natural deduction as resolution

• Main Author: Robinson, David Edward Ashdown
• Published: University of Manchester 2009
• Subjects: 006.3
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.515225

This thesis studies deduction systems for modal logics and the relation between them. Natural deduction systems give proofs that are close to human reasoning but are not well suited to automation while refutation systems are well suited to automation but inference steps are not close to human informal reasoning. This thesis will introduce a natural deduction calculus with a resolution rule that gives a good framework for simulating different calculi and studying their properties. We show that this calculus is able to directly simulate a tableau calculus for modal logic using two different search strategies. We then introduce an ordered hyperresolution calculus for modal logic K using a structural transformation to preserve structure of input formulae. We show that there is a mapping from derivations in the ordered hyperresolution calculus to derivations in the natural deduction calculus and a further mapping in the other direction. The hyperresolution calculus is a standard calculus and we show that it is therefore possible to automatically generate proofs dose to human reasoning using already existing, fast theorem provers. We give extensions of the structural transformation to a number of extensions of K and show that the mappings in both directions still hold. Since we have two simulations in a common framework, the relation between the tableau and resolution simulation are considered.