Geodesic
Proof search algorithm in pure logical framework
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 17 (2020), pp. 988-998

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: automated deduction, logical framework. 
@article{SEMR_2020_17_a20,
     author = {D. Yu. Vlasov},
     title = {Proof search algorithm in pure logical framework},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {988--998},
     publisher = {mathdoc},
     volume = {17},
     year = {2020},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2020_17_a20/}
}
TY  - JOUR
AU  - D. Yu. Vlasov
TI  - Proof search algorithm in pure logical framework
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2020
SP  - 988
EP  - 998
VL  - 17
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2020_17_a20/
LA  - en
ID  - SEMR_2020_17_a20
ER  - 
%0 Journal Article
%A D. Yu. Vlasov
%T Proof search algorithm in pure logical framework
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2020
%P 988-998
%V 17
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2020_17_a20/
%G en
%F SEMR_2020_17_a20
D. Yu. Vlasov. Proof search algorithm in pure logical framework. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 17 (2020), pp. 988-998. http://geodesic.mathdoc.fr/item/SEMR_2020_17_a20/