39
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic

      Preprint
      , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Inspired by the recent evolution of deep neural networks (DNNs) in machine learning, we explore their application to PL-related topics. This paper is the first step towards this goal; we propose a proof-synthesis method for the negation-free propositional logic in which we use a DNN to obtain a guide of proof search. The idea is to view the proof-synthesis problem as a translation from a proposition to its proof. We train seq2seq, which is a popular network in neural machine translation, so that it generates a proof encoded as a \(\lambda\)-term of a given proposition. We implement the whole framework and empirically observe that a generated proof term is close to a correct proof in terms of the tree edit distance of AST. This observation justifies using the output from a trained seq2seq model as a guide for proof search.

          Related collections

          Most cited references5

          • Record: found
          • Abstract: not found
          • Article: not found

          Context-Dependent Pre-Trained Deep Neural Networks for Large-Vocabulary Speech Recognition

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Simple Fast Algorithms for the Editing Distance between Trees and Related Problems

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              The calculus of constructions

                Bookmark

                Author and article information

                Journal
                2017-06-20
                Article
                1706.06462
                3e38e67f-6338-4fef-972d-db0ebed64284

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                cs.PL cs.AI cs.LO

                Theoretical computer science,Programming languages,Artificial intelligence
                Theoretical computer science, Programming languages, Artificial intelligence

                Comments

                Comment on this article