[isabelle] Tableaux 2015, second call for papers

Dear Isabelle List,

Tableaux 2015 is now waiting for submissions -- on a variety of topics, including the intersection between automatic and interactive theorem proving.

All the best,



24th International Conference on Automated Reasoning with
Analytic Tableaux and Related Methods

Wroclaw, Poland, September 21-24, 2015


TABLEAUX 2015 is the 24th in the series of international meetings
on Automated Reasoning with Analytic Tableaux and Related Methods,
and will be held in Wroclaw, Poland, during September 21-24, 2015.

TABLEAUX 2015 will be co-located with the 10th International Symposium
on Frontiers of Combining Systems (FroCoS 2015).

The computer science institute of Wroclaw has a large experience
in hosting international conferences. It has hosted
the IEEE Symposium on Logic in Computer Science (LICS 2007),
the 24th International Conference on Automated Deduction
(CADE 2011), and the 22nd European Symposium on Algorithms (ALGO 2014).

Tableaux methods offer a convenient and flexible set of tools
for automated reasoning in classical logic, extensions of classical
logic, and a large number of non-classical logics. For large
groups of logics, tableaux methods can be generated automatically.
Areas of application include verification of software and computer
systems, deductive databases, knowledge representation and its required
inference engines, teaching, and system diagnosis.
The conference series aims to bring together researchers interested in all
aspects of tableaux - theoretical foundations, applications,
and implementation techniques.

* tableaux methods for classical and non-classical logics
(e.g. modal, temporal, description, intuitionistic, substructural,
fuzzy, paraconsistent logics) and their proof theoretic
* related methods (model elimination, model checking, connection
methods, resolution, BDDs).
* sequent calculi for classical and non-classical logics,
as tools for proof search and proof representation.
* flexible, easily extendable, light weight methods for theorem proving.
* novel types of calculi for theorem proving and verification
in classical and non-classical logics.
* systems, tools, implementations and applications (provers,
logical frameworks, model checkers, ... ).
* implementation techniques (data structures, efficient algorithms,
performance measurement, extendibility, ... ).
* extensions of tableaux procedures with conflict-driven learning,
generation of proofs; compact (or humanly readable) representation
of proofs.
* decision procedures, theoretically optimal procedures.
* applications of automated deduction to mathematics, software
development, protocol verification, or teaching.

TABLEAUX 2015 also welcomes papers describing applications of tableaux
procedures to real world examples. Such papers should be tailored to
the tableaux community and should focus on the role of reasoning,
and logical aspects of the solution.

Submissions are invited in two categories:

A Research papers, which describe original theoretical research,
original algorithms, or applications, with length
up to 15 pages.
B System descriptions, with length up to 10 pages.

Submissions will be reviewed by the PC, possibly will help of
external reviewers, taking into account readability, relevance
and originality.

For category A, theoretical results and algorithms must be original,
and not submitted for publication elsewhere. Submissions will be reviewed
taking into account correctness, theoretical prettyness, and possible

For category B submissions, a working implementation
must be available on the internet, which includes sources.
The aim of a system description is to make the system available
in such a way that users can use it, understand it, and build on it.

Accepted papers in both categories will be published in the conference
proceedings (within the LNAI series of Springer).

For accepted papers in both of the categories, at least one author
is required to attend the conference and present the paper.

Further information and instructions about submissions can be found
on the conference website http://tableaux2015.ii.uni.wroc.pl<http://tableaux2015.ii.uni.wroc.pl/>


Abstract submission deadline: May 8th, 2015
Paper submission deadline: May 15th, 2015
Author Notification: July 1st, 2015
Final Version: July 17th 2015
Conference: September 21st-24th, 2015


Marc Bezem, University of Bergen, Norway
Agata Ciabattoni, Vienna University of Technology, Austria
David Delahaye, National Conservatory of Arts and Professions, Paris,
Ulrich Furbach, University of Koblenz, Germany
Didier Galmiche, Universite de Lorraine, Nancy, France
Silvio Ghilardi, Universita degli Studi di Milano, Italy
Rajeev Gore, Australian National University, Canberra, Australia
Stephane Graham-Lengrand, Ecole Polytechnique, Palaiseau, France
Reiner Haehnle, Darmstadt University of Technology, Germany
Konstantin Korovin, University of Manchester, UK
George Metcalfe, University of Bern, Switzerland
Dale Miller, INRIA Saclay-Ile-de-France, France
Barbara Morawska, Technische Universitaet Dresden, Germany
Boris Motik, University of Oxford, UK
Claudia Nalon, University of Brasilia, Brasil
Sara Negri, University of Helsinki, Finland
Linh Anh Nguyen, University of Warsaw, Poland
Hans de Nivelle (chair), University of Wroclaw, Poland
Jens Otten, University of Potsdam, Germany
Andrei Popescu, Middlesex University London, UK
Renate Schmidt, University of Manchester, UK
Luca Vigano, King's College, London, UK
Bruno Woltzenlogel-Paleo, Vienna University of Technology, Austria


Workshops have been solicited in separate call, which can
be found on http://tableaux2015.ii.uni.wroc.pl<http://tableaux2015.ii.uni.wroc.pl/> or

Tutorials for FroCoS/TABLEAUX will be solicited in a separate call, which
will be published later.


Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.

If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS.  There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.