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/

[1] C.L. Chang, R.C. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York-London, 1973 | MR | Zbl

[2] V. Davydov, S. Maslov, G. Mints, V. Orevkov, A. Slissenko, “A computer algorithm of establisihing deducibility based on the inverse method”, Zap. Nauchn. Semin. LOMI, 16, 1969, 1–16 | MR | Zbl

[3] A. Degtyarev, A. Voronkov, “The Inverse Method”, Handbook of Automated Reasoning, ch. 4, v. 1, Elsevier, Amsterdam, 2001, 179–272 | DOI | Zbl

[4] I.V. Ramakrishnan, R.Sekar, A. Voronkov, “Term indexing”, Handbook of Automated Reasoning, ch. 26, v. 2, Elsevier, Amsterdam, 2001, 1853–1964 | MR | Zbl

[5] M.J.C. Gordon, “Representing a logic in the LCF metalanguage”, Tools and Notions for Program Construction: an Advanced Course, Cambridge University Press, 1982, 263–185

[6] J. Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, Cambridge, 2009 | MR | Zbl

[7] S. Maslov, “An inverse method of establishing deducibility in classical predicate calculus”, Sov. Math. Dokl., 5 (1965), 1420–1424 | MR | Zbl

[8] N. Megill, Metamath: A Computer Language for Pure Mathematics, Lulu press, Morrisville, North Carolina, 2007

[9] E. Post, “Formal Reductions of the General Combinatorial Decision Problem”, Am. J. Math., 65:2 (1943), 197–215 | DOI | MR | Zbl

[10] D. Prawitz, H. Prawitz, N. Voghera, “A mechanical proof procedure and its realization in an electronic computer”, J. ACM, 7:2 (1960), 102–128 | DOI | MR | Zbl

[11] J.A. Robinson, “A machine-oriented logic based on the resolution principle”, J. ACM, 12:1 (1965), 23–41 | DOI | MR | Zbl