References & Citations
Mathematics > Logic
Title: Proof Search Algorithm in Pure Logical Framework
(Submitted on 17 Oct 2017 (v1), last revised 3 Dec 2017 (this version, v2))
Abstract: By a pure logical framework we mean a framework which does not rely on any particular formal calculus. For example, Metamath is an instance of a pure logical framework. Another example is the Russell system (this https URL). In this paper, we describe the proof search algorithm used in Russell. The algorithm is proved to be correct and complete, i.e. it gives only valid proofs and any valid proof can be found (up to a substitution) by the proposed algorithm.
Submission history
From: Dmitry Vlasov [view email][v1] Tue, 17 Oct 2017 09:29:54 GMT (33kb)
[v2] Sun, 3 Dec 2017 15:09:27 GMT (33kb)
Link back to: arXiv, form interface, contact.