From tancs@dis.uniroma1.it Fri Sep 24 16:56:43 1999 Date: Fri, 24 Sep 1999 10:49:44 PDT From: TANCS 2000 Reply-To: Theory-A - TheoryNet World-Wide Events , TANCS 2000 To: THEORYNT@LISTSERV.NODAK.EDU Subject: TANCS 2000 - First Call for Experimental Papers Apologies for multiple copies... %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% First %% %% Call for Experimental Papers %% %% TANCS 2000 %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TABLEAUX Non Classical Systems Comparison Experimental Analysis of Theorem Provers and Satisfiability Testers on Non Classical Logics at the 7th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) University of St Andrews St Andrews, Scotland July 4-7, 2000 (further details at http://www.dis.uniroma1.it/~tancs) The TABLEAUX conferences are a major forum for the presentation of new research in all aspects of automated deduction. In order to stimulate Automated Theorem Proving and Satisfiability Testing development in non classical logics, and to expose ATP systems to interested researchers, the TANC Systems Comparison will be held at TABLEAUX-00 on July 4-7, 2000. See the main TABLEAUX page for general details about this series of conferences: it is at http://i12www.ira.uka.de/TABLEAUX/ ** What is the TABLEAUX Non Classical Systems Comparison ** The aim of TANCS is to compare the performance of fully automatic, non classical ATP systems (based on tableaux, resolution, rewriting, ...) in an experimental setting and promote the experimental study on theorem proving and satisfiability testing in non classical logics. For TANCS-2000 the focus is on extended modal and description logics and in particular benchmarks derived from combinatorial problems will be available for: - modal logic K without global axioms (description logic ALC) - modal logic K with global axioms (ALC with cyclic TBox) - basic temporal logic Kt (ALC with inverse roles) - basic temporal logic Kt with global axioms (ALC with inverse and TBoxes) This year new benchmarks will be available for Converse Propositional Dynamic Logic. ** Who can take part? ** Everybody who has written a prover for one of the logics under consideration. There is no restriction to provers that use a particular calculus. In particular we welcome novel approaches based on tableaux, resolution, rewriting, automata, and SAT-based decision procedure. ** Experimental papers and provers submission ** Submissions are invited as original, unpublished experimental papers describing a theorem prover and its performance on the benchmarks of the TANCS 2000 Comparison. Beside the paper, entrants are requested to submit the executable (or source code) of their prover and a summary of the experimental data upon which their paper is based. The experimental papers, together with information on the comparison design and results, will appear in the proceedings of the TABLEAUX-2000 conference published by Springer Verlag in the LNAI series. ** How submitted systems will be compared? ** The comparison will be mainly based on two aspects: Effectiveness, measured by the type and number of problems solved, the average runtime for successful solutions the scaling of the prover as problems get bigger Usability, measured by the availability of the prover via web or other sources the portability of the code to various platforms the ease of installation and use ** Important Dates ** Deadlines for submission: January, 19, 2000 Evaluation of Results: February 10, 2000 Deadline for final text: March 10, 2000 TABLEAUX-00: July 4-7, 2000 ** Information ** TANCS-2000 E-mail: tancs@dis.uniroma1.it WWW: http://www.dis.uniroma1.it/~tancs Comparison Chair: Fabio Massacci Dip. di Ingegneria dell'Informazione Universita di Siena via Roma 56, 53100 Siena Italy Phone: +39-0577-234607 Fax: +39-0577-233602 TABLEAUX-2000 E-mail: rd@dcs.st-and.ac.uk WWW: http://www.dcs.st-and.ac.uk/~tab2000 Program Chair: Roy Dyckhoff TABLEAUX 2000 Program Chair Computer Science Division University of St Andrews St Andrews, Fife, KY16 9SS Scotland Phone: +44-1334-463267 Fax: +44-1334-463278