<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//TaxonX//DTD Taxonomic Treatment Publishing DTD v0 20100105//EN" "../../nlm/tax-treatment-NS0.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:tp="http://www.plazi.org/taxpub" article-type="research-article" dtd-version="3.0" xml:lang="en">
  <front>
    <journal-meta>
      <journal-id journal-id-type="publisher-id">109</journal-id>
      <journal-id journal-id-type="index">urn:lsid:arphahub.com:pub:3dc5f44e-8666-58db-bc76-a455210e8891</journal-id>
      <journal-title-group>
        <journal-title xml:lang="en">JUCS - Journal of Universal Computer Science</journal-title>
        <abbrev-journal-title xml:lang="en">jucs</abbrev-journal-title>
      </journal-title-group>
      <issn pub-type="ppub">0948-695X</issn>
      <issn pub-type="epub">0948-6968</issn>
      <publisher>
        <publisher-name>Journal of Universal Computer Science</publisher-name>
      </publisher>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="doi">10.3217/jucs-005-03-0088</article-id>
      <article-id pub-id-type="publisher-id">27541</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Connection-Based Theorem Proving in Classical and Non-Classical Logics</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Kreitz</surname>
            <given-names>Christoph</given-names>
          </name>
          <email xlink:type="simple">kreitz@cs.cornell.edu</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Otten</surname>
            <given-names>Jens</given-names>
          </name>
          <xref ref-type="aff" rid="A2">2</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">Department of Computer Science, Cornell-University, Ithaca, NY, United States of America</addr-line>
        <institution>Department of Computer Science, Cornell-University</institution>
        <addr-line content-type="city">Ithaca, NY</addr-line>
        <country>United States of America</country>
      </aff>
      <aff id="A2">
        <label>2</label>
        <addr-line content-type="verbatim">FG Intellektik, FB Informatik, Darmstadt University of Technology, Darmstadt, Germany</addr-line>
        <institution>FG Intellektik, FB Informatik, Darmstadt University of Technology</institution>
        <addr-line content-type="city">Darmstadt</addr-line>
        <country>Germany</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Christoph Kreitz (<email xlink:type="simple">kreitz@cs.cornell.edu</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>1999</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>03</month>
        <year>1999</year>
      </pub-date>
      <volume>5</volume>
      <issue>3</issue>
      <fpage>88</fpage>
      <lpage>112</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/2D3BF670-46AB-5B2E-B6A9-5FA7D7B736E1">2D3BF670-46AB-5B2E-B6A9-5FA7D7B736E1</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6995652">6995652</uri>
      <permissions>
        <copyright-statement>Christoph Kreitz, Jens Otten</copyright-statement>
        <license license-type="creative-commons-attribution" xlink:href="" xlink:type="simple">
          <license-p>This article is freely available under the J.UCS Open Content License.</license-p>
        </license>
      </permissions>
      <abstract>
        <label>Abstract</label>
        <p>We present a uniform procedure for proof search in classical logic, intuitionistic logic, various modal logics, and fragments of linear logic. It is based on matrix characterizations of validity in these logics and extends Bibel's connection method, originally developed for classical logic, accordingly. Besides combining a variety of different logics it can also be used to guide the development of proofs in interactive proof assistants and shows how to integrate automated and interactive theorem proving.</p>
      </abstract>
    </article-meta>
  </front>
</article>
