<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.3 20210610//EN" "https://jats.nlm.nih.gov/publishing/1.3/JATS-journalpublishing1-3.dtd">
<article article-type="research-article" dtd-version="1.3" xml:lang="en">
  <front>
    <journal-meta>
      <journal-title-group>
        <journal-title>Computing, Telecommunication and Control</journal-title>
        <trans-title-group xml:lang="ru">
          <trans-title>Информатика, телекоммуникации и управление</trans-title>
        </trans-title-group>
      </journal-title-group>
      <issn pub-type="epub">2687-0517</issn>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="publisher-id">7</article-id>
      <article-id pub-id-type="doi">10.5862/JCSTCS.234.7</article-id>
      <title-group>
        <article-title>An Experimental Computer Program for Automated Reasoning in Intuitionistic Logic Using the Inverse Method</article-title>
        <trans-title-group xml:lang="ru">
          <trans-title>Экспериментальная программа для доказательства теорем интуиционистской логики обратным методом Маслова</trans-title>
        </trans-title-group>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <name>
            <surname>Pavlov</surname>
            <given-names>Vladimir</given-names>
          </name>
          <email>vlapav239@gmail.com</email>
        </contrib>
        <contrib contrib-type="author">
          <name>
            <surname>Pak</surname>
            <given-names>Vadim</given-names>
          </name>
          <email>vadimpak917@gmail.com</email>
        </contrib>
      </contrib-group>
      <pub-date publication-format="electronic" date-type="pub" iso-8601-date="2015-12-10">
        <day>10</day>
        <month>12</month>
        <year>2015</year>
      </pub-date>
      <issue>6</issue>
      <issue-id pub-id-type="publisher-id">234</issue-id>
      <fpage>70</fpage>
      <lpage>80</lpage>
      <abstract xml:lang="en">
        <p>We discuss the inverse method of automated theorem-proving that was invented by S. Maslov. The inverse method can be applied to various logics: propositional logic, first-order logic, modal logics, intuitionistic logic, etc. In the current article, we present an overview of the key publications on the inverse method, describe in detail an inverse method calculus for first-order intuitionistic logic. We propose adapted as well as original optimizing strategies for the developed calculus. We discuss a proof search algorithm for the proposed calculus and our program implementation named WhaleProver. We compare WhaleProver with state-of-the-art intuitionistic theorem provers on problems from the ILTP library, which is a common benchmarking library for testing intuitionistic theorem provers.</p>
      </abstract>
      <kwd-group xml:lang="en">
        <kwd>automated theorem proving</kwd>
        <kwd>sequent calculus</kwd>
        <kwd>inverse method</kwd>
        <kwd>intuitionistic logic</kwd>
        <kwd>ILTP</kwd>
      </kwd-group>
    </article-meta>
  </front>
</article>
