[om-a] TANCS 2000 - First Call for Experimental Papers

[TANCS 2000]

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 at 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 at 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
--
om-announce at openmath.org  -  public announcements concerning OpenMath
Post discussion to om at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-announce-owner at openmath.org for assistance with any problems