Issues in the Analysis of Proof-Search Strategies in Sequential Presentations of Logics |
| |
Authors: | Tatjana Lutovac James Harland |
| |
Affiliation: | School of Computer Science and Information Technology, RMIT University, GPO Box 2476V, Melbourne, 3001, Australia |
| |
Abstract: | Many proof search strategies can be expressed as restrictions on the order of application of the rules of the sequent calculus. Properties of these strategies are then shown by permutation arguments, such as showing that a given strategy is complete by transforming an arbitrary proof into one which obeys the strategy. Such analyses involve some very tedious manipulations of proofs, and are potentially overwhelming for humans. In this paper we investigate the development of systematic techniques for the analysis of sequent calculi. We show how a particular specification of inference rules leads to a detailed analysis of permutation properties for these rules, and we also investigate how to detect redundancies in proofs resulting from these rules. |
| |
Keywords: | Proof search affine logic linear logic loop detection |
本文献已被 ScienceDirect 等数据库收录! |