<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Automated Reasoning in Quantified Non-Classical Logics</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>rd International Workshop</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>ARQNL</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Oxford</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>United Kingdom</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Christoph Benzmu ̈ ller University of Luxembourg (and Freie Universita ̈t Berlin) Avenue de l'Universite ́</institution>
          ,
          <addr-line>L-4365 Esch-sur-Alzette</addr-line>
          ,
          <country country="LU">Luxembourg</country>
        </aff>
        <aff id="aff1">
          <label>1</label>
          <institution>Jens Otten University of Oslo PO</institution>
          <addr-line>Box 1080 Blindern, 0316 Oslo</addr-line>
          ,
          <country country="NO">Norway</country>
        </aff>
      </contrib-group>
      <pub-date>
        <year>2095</year>
      </pub-date>
      <volume>2095</volume>
      <fpage>5</fpage>
      <lpage>8</lpage>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>Proceedings CEUR Workshop Proceedings, Volume 2095</title>
      <sec id="sec-1-1">
        <title>Preface</title>
        <p>This volume contains the proceedings of the Third International Workshop on Automated
Reasoning in Quantified Non-Classical Logics (ARQNL 2018), held July 18th, 2018, in Oxford,
United Kingdom. The workshop was affiliated and co-located with the International Joint
Conference on Automated Reasoning (IJCAR 2018), which was part of the Federated Logic
Conference (FLoC 2018). The aim of the ARQNL 2018 Workshop has been to foster the
development of proof calculi, automated theorem proving (ATP) systems and model finders for
all sorts of quantified non-classical logics. The ARQNL workshop series provides a forum for
researchers to present and discuss recent developments in this area.</p>
        <p>Non-classical logics — such as modal logics, conditional logics, intuitionistic logic,
description logics, temporal logics, linear logic, multivalued logic, dynamic logic, deontic logic,
fuzzy logic, paraconsistent logic, relevance logic, free logic, natural logic — have many
applications in AI, Computer Science, Philosophy, Linguistics, and Mathematics. Hence, the
automation of proof search in these logics is a crucial task. For many propositional non-classical
logics there exist proof calculi and ATP systems. But proof search is significantly more difficult
than in classical logic. For first-order and higher-order non-classical logics the mechanization
and automation of proof search is even more difficult. Furthermore, extending existing
nonclassical propositional calculi, proof techniques and implementations to quantified logics is
often not straightforward. As a result, for most quantified non-classical logics there exist no
or only few (efficient) ATP systems. It is in particular the aim of the ARQNL workshop
series to initiate and foster practical implementations and evaluations of such ATP systems for
non-classical logics.</p>
        <p>The ARQNL 2018 Workshop received eight paper submissions. Each paper was reviewed
by at least three referees, and following an online discussion, six research papers were selected
to be included in the proceedings. The ARQNL 2018 Workshop also included invited talks by
Larry Moss and Giles Reger. Additionally, one research paper was selected for presentation at
the workshop.</p>
        <p>We would like to sincerely thank the invited speakers and all authors for their contributions.
We would also like to thank the members of the Program Committee of ARQNL 2018 for their
professional work in the review process. Furthermore, we would like to thank the IJCAR
Workshop Chair Alberto Griggio and the Organizing Committee of FLoC 2018. Finally, many
thanks to all active participants of the ARQNL 2018 Workshop.</p>
        <sec id="sec-1-1-1">
          <title>Luxembourg and Oslo, July 2018</title>
        </sec>
        <sec id="sec-1-1-2">
          <title>Christoph Benzmu¨ller Jens Otten</title>
        </sec>
      </sec>
      <sec id="sec-1-2">
        <title>Organization</title>
      </sec>
    </sec>
    <sec id="sec-2">
      <title>Program Committee</title>
      <sec id="sec-2-1">
        <title>Christoph Benzmu¨ ller</title>
        <p>Jose´ Luiz Fiadeiro
Marcelo Finger
Didier Galmiche
Rajeev Gore´
Andreas Herzig
Sven Linker
Aniello Murano
Hans De Nivelle
Jens Otten
Valeria De Paiva
Xavier Parent
Revantha Ramanayake
Giselle Reis
Leila Ribeiro
Bruno Woltzenlogel Paleo</p>
      </sec>
    </sec>
    <sec id="sec-3">
      <title>Workshop Chairs</title>
      <p>University of Luxembourg &amp; FU Berlin, Germany – co-chair
Royal Holloway University of London
University of Sa˜o Paulo, Brazil
Universite´ de Lorraine - LORIA, France
The Australian National University, Australia
IRIT-CNRS, France
University of Liverpool, UK
Universita` di Napoli “Federico II”, Italy
Nazarbayev University, Kazakhstan
University of Oslo, Norway – co-chair
Nuance Communications, UK
University of Luxembourg, Luxembourg
Vienna University of Technology, Austria
Carnegie Mellon University, Qatar
Universidade Federal do Rio Grande do Sul, Brazil
Vienna University of Technology, Austria</p>
      <sec id="sec-3-1">
        <title>Contents</title>
        <sec id="sec-3-1-1">
          <title>Implementations of Natural Logics</title>
          <p>Lawrence S. Moss
Some Thoughts About FOL-Translations in Vampire
Giles Reger</p>
        </sec>
        <sec id="sec-3-1-2">
          <title>Pseudo-Propositional Logic</title>
          <p>Ahmad-Saher Azizi-Sultan
A Simple Semi-automated Proof Assistant for First-order Modal Logics
Tomer Libal
Labelled Connection-based Proof Search for Multiplicative Intuitionistic
Linear Logic
Didier Galmiche and Daniel Me´ry
Labelled Calculi for Quantified Modal Logics with Non-rigid and
Nondenoting Terms
Eugenio Orlandelli and Giovanna Corsi
System Demonstration: The Higher-Order Prover Leo-III
Alexander Steen and Christoph Benzmu¨ller
Evidence Extraction from Parameterised Boolean Equation Systems
Wieger Wesselink and Tim A.C. Willemse
1–10
11–25
26–33
34–48
49–63
64–78
79–85</p>
        </sec>
      </sec>
    </sec>
  </body>
  <back>
    <ref-list />
  </back>
</article>