2 papers
math.LO2017
System Description: Russell - A Logical Framework for Deductive Systems
Dmitry Vlasov
Russell is a logical framework for the specification and implementation of deductive systems. It is a high-level language with respect to Metamath language, so inherently it uses a…
math.LO2017
Proof Search Algorithm in Pure Logical Framework
Dmitry Vlasov
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 exa…