Geodesic
Two-level realization of logical formulas for deductive program synthesis
Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹûternye nauki, Tome 34 (2024) no. 4, pp. 469-485 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

This paper presents a novel approach to interpreting logical formulas for synthesizing algorithms and programs. The proposed method combines features of Kleene realizability and Gödel's “dialectica” interpretation but does not rely on them directly. A simple version of positive predicate logic without functions is considered, including conjunction, disjunction, implication, and universal and existential quantifiers. A new realizability semantics for formulas and sequents is described, which considers not just a realization of a formula, but a realization with additional support. The realization roughly corresponds to Kleene realizability. The support provides additional data in favor of the correctness of the realization. The support must confirm that the realization works correctly for the formula under any valid conditions of application. A proof language is presented for which a correctness theorem is proved showing that any derivable sequent has a realization and support confirming that this realization works correctly for this formula under any valid conditions with a suitable interpreter for the programs used.
Keywords: logical formulas, algorithm synthesis, program synthesis, predicate logic, calculus of sequents, proofs, interpretation of logical formulas, artificial intelligence 
@article{VUU_2024_34_4_a0,
     author = {M. Joudakizadeh and A. P. Bel'tyukov},
     title = {Two-level realization of logical formulas for deductive program synthesis},
     journal = {Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹ\^uternye nauki},
     pages = {469--485},
     year = {2024},
     volume = {34},
     number = {4},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/VUU_2024_34_4_a0/}
}
TY  - JOUR
AU  - M. Joudakizadeh
AU  - A. P. Bel'tyukov
TI  - Two-level realization of logical formulas for deductive program synthesis
JO  - Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹûternye nauki
PY  - 2024
SP  - 469
EP  - 485
VL  - 34
IS  - 4
UR  - http://geodesic.mathdoc.fr/item/VUU_2024_34_4_a0/
LA  - en
ID  - VUU_2024_34_4_a0
ER  - 
%0 Journal Article
%A M. Joudakizadeh
%A A. P. Bel'tyukov
%T Two-level realization of logical formulas for deductive program synthesis
%J Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹûternye nauki
%D 2024
%P 469-485
%V 34
%N 4
%U http://geodesic.mathdoc.fr/item/VUU_2024_34_4_a0/
%G en
%F VUU_2024_34_4_a0
M. Joudakizadeh; A. P. Bel'tyukov. Two-level realization of logical formulas for deductive program synthesis. Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹûternye nauki, Tome 34 (2024) no. 4, pp. 469-485. http://geodesic.mathdoc.fr/item/VUU_2024_34_4_a0/

[1] Gulwani S., Polozov O., Singh R., “Program synthesis”, Foundations and Trends® in Programming Languages, 4:1–2 (2017), 1–119 | DOI

[2] Alur R., Bodik R., Juniwal G., Martin M. M. K., Raghothaman M., Seshia S. A., Singh R., Solar-Lezama A., Torlak E., Udupa A., “Syntax-guided synthesis”, 2013 Formal Methods in Computer-Aided Design, IEEE, Portland, 2013, 1–8 | DOI

[3] Kleene S.C., “On the interpretation of intuitionistic number theory”, The Journal of Symbolic Logic, 10:4 (1945), 109–124 | DOI | MR | Zbl

[4] Gödel K., “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes”, Dialectica, 12:3–4 (1958), 280–287 | DOI | MR | Zbl

[5] Seshia S.A., Desai A., Dreossi T., Fremont D.J., Ghosh S., Kim E., Shivakumar S., Vazquez-Chanlatte M., Yue Xiangyu, “Formal specification for deep neural networks”, Automated Technology for Verification and Analysis, 16th International Symposium, ATVA 2018 (Los Angeles, CA, USA, October 7–10, 2018), Proceedings, Springer, Cham, 2018, 20–34 | DOI | MR | Zbl

[6] Handbook of proof theory, eds. Buss S.R., Elsevier, Amsterdam, 1998 | MR | Zbl

[7] Shanin N.A., “A constructive interpretation of mathematical judgments”, Trudy Matematicheskogo Instituta imeni V.A. Steklova, 52 (1958), 226–311 (in Russian) | Zbl

[8] Kohlenbach U., “Gödel’s functional interpretation and its use in current mathematics”, Dialectica, 62:2 (2008), 223–267 | DOI | MR

[9] Solar-Lezama A., Rabbah R., Bodík R., Ebcioğlu K., “Programming by sketching for bit-streaming programs”, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, Association for Computing Machinery, 2005, 281–294 | DOI

[10] Hoare C.A.R., “An axiomatic basis for computer programming”, Communications of the ACM, 12:10 (1969), 576–580 | DOI | MR | Zbl

[11] Dijkstra E.W., “Guarded commands, nondeterminacy and formal derivation of programs”, Communications of the ACM, 18:8 (1975), 453–457 | DOI | MR | Zbl

[12] Srivastava S., Gulwani S., Foster J.S., “From program verification to program synthesis”, Proceedings of the 37th Annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Association for Computing Machinery, 2010, 313–326 | DOI | Zbl

[13] Katz G., Barrett C., Dill D.L., Julian K., Kochenderfer M.J., “Reluplex: An efficient SMT solver for verifying deep neural networks”, Computer Aided Verification, 29th International Conference, CAV, 2017 (Heidelberg, Germany, July 24–28, 2017), Proceedings, Part I, Springer, Cham, 2017, 97–117 | DOI | MR | Zbl

[14] Guidotti R., Monreale A., Ruggieri S., Turini F., Giannotti F., Pedreschi D., “A survey of methods for explaining black box models”, ACM Computing Surveys (CSUR), 51:5 (2018), 93, 1–42 | DOI

[15] Schkufza E., Sharma R., Aiken A., “Stochastic superoptimization”, ACM SIGARCH Computer Architecture News, 41:1 (2013), 305–316 | DOI