=Paper=
{{Paper
|id=Vol-1770/ARQNL2016_preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1770/ARQNL2016_preface.pdf
|volume=Vol-1770
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-1770/ARQNL2016_preface.pdf</pdf>
<pre>
Christoph Benzmüller
Jens Otten (Eds.)


Automated Reasoning in
Quantified Non-Classical Logics

2nd International Workshop, ARQNL 2016,
Coimbra, Portugal, July 1st, 2016


Proceedings


CEUR Workshop Proceedings, Volume 1770
Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016)


                                       Preface


This volume contains the proceedings of the Second International Workshop on Au-
tomated Reasoning in Quantified Non-Classical Logics (ARQNL 2016), held July 1st,
2016, in Coimbra, Portugal. The workshop was affiliated and co-located with the In-
ternational Joint Conference on Automated Reasoning (IJCAR 2016). The aim of the
ARQNL 2016 Workshop has been to foster the development of proof calculi, auto-
mated 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.
    Non-classical logics — such as modal logics, conditional logics, intuitionistic logic,
description logics, temporal logics, linear logic, dynamic logic, fuzzy logic, paraconsis-
tent logic, relevance logic — have many applications in AI, Computer Science, Philos-
ophy, 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 significant more difficult than in clas-
sical logic. For first-order and higher-order non-classical logics the mechanization and
automation of proof search is even more difficult. Furthermore, extending existing
non-classical 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 AR-
QNL workshop series to initiate and foster practical implementations and evaluations
of such ATP systems for non-classical logics.
    The ARQNL 2016 Workshop received 6 paper submissions. Each paper was re-
viewed by at least three referees, and following an online discussion, 5 research papers
were selected to be included in the proceedings. The ARQNL 2016 Workshop also
included an invited talk by Revantha Ramanaya.
    We would like to sincerely thank the invited speaker and all authors for their con-
tributions. We would also like to thank the members of the Program Committee of
ARQNL 2016 for their professional work in the review process. Furthermore, we would
like to thank the Workshop Chair Reinhard Kahle and the Organizing Committee of
IJCAR 2016. Finally, many thanks to all active participants of the ARQNL 2016
Workshop.


                                                                      Christoph Benzmüller
Berlin and Oslo, July 2016
                                                                                Jens Otten


                                             ii
Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016)


                                  Organization

Program Committee

Carlos Areces                Universidad Nacional de Córdoba, Argentina
Christoph Benzmüller        Freie Universität Berlin, Germany – co-chair
Walter Carnielli             Centre for Logic, Epistemology and the History of Science,
                             Brazil
Christian Fermüller         TU Wien, Austria
Rajeev Goré                 The Australian National University, Australia
Andreas Herzig               IRIT-CNRS, France
Stephan Merz                 INRIA Nancy, France
Till Mossakowski             University of Magdeburg, Germany
Aniello Murano               Università di Napoli “Federico II”, Italy
Hans De Nivelle              University of Wroclaw, Poland
Jens Otten                   University of Oslo, Norway – co-chair
Valeria De Paiva             University of Birmingham, UK
Giselle Reis                 INRIA Saclay, France
Julian Richardson            Google Inc., USA
Luca Viganò                 King’s College London, UK


Workshop Chairs

Christoph Benzmüller
Freie Universität Berlin
Arnimallee 7, 14195 Berlin, Germany
E-mail: c.benzmueller@fu-berlin.de


Jens Otten
University of Oslo
PO Box 1080 Blindern, 0316 Oslo, Norway
E-mail: jeotten@ifi.uio.no


                                             iii
Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016)


                                     Contents

From Axioms to Proof Rules, Then Add Quantifiers                       1–8
Revantha Ramanayake

Non-clausal Connection-based Theorem Proving in Intuitionistic
   First-Order Logic                                                  9–20
Jens Otten

Sequent Calculi for Indexed Epistemic Logics                          21–35
Giovanna Corsi and Eugenio Orlandelli

A Dynamic Logic for Configuration                                     36–50
Ching Hoo Tang and Christoph Weidenbach

TPTP and Beyond: Representation of Quantified Non-Classical Logics    51–65
Max Wisniewski, Alexander Steen and Christoph Benzmüller

Optimizing Inconsistency-tolerant Description Logic Reasoning         66–80
Mokarrom Hossain and Wendy MacCaull


                                             iv

</pre>