PROOF SEARCH ALGORITHM IN PURE LOGICAL FRAMEWORK

A pure logical framework is a logical framework which does not rely on any particular formal calculus. For example, Metamath (http://metamath.org) is an instance of a pure logical framework. Another example is the Russell system (https://github.com/dmitry-vlasov/russell-flow), which may be considered a high-level language based on Metamath. In this paper, we describe the proof search algorithm used in Russell. The algorithm is proved to be sound and complete, i.e. it gives only valid proofs and any valid proof can be found (up to a substitution) by the proposed algorithm.