| CADE-19 in Miami28 July - 2 August 2003In the sunshine ... On the beach |
|
|
| CADE-19 in Miami28 July - 2 August 2003In the sunshine ... On the beach |
|
CADE-19 invites paper submissions related to all aspects of automated deduction, including foundations, implementations, and applications.
Logics of interest include propositional, first-order, equational, higher-order, classical, intuitionistic, constructive, modal, temporal, many-valued, substructural, description, and meta-logics, logical frameworks, type theory and set theory.
Methods of interest include saturation, resolution, tableaux, sequent calculi, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, natural deduction, proof planning, proof presentation, proof checking, and explanation.
Applications of interest include hardware and software development, systems analysis and verification, deductive databases, functional and logic programming, computer mathematics, natural language processing, computational linguistics, robotics, planning, knowledge representation, and other areas of AI.
Original research papers, papers on applications of automated deduction methods and tools, and descriptions of working automated deduction systems are solicited. The different kinds of submissions are evaluated according to different criteria, which are described below.
Conference submission is electronic in postscript or PDF format. Submitted papers must conform to the Springer LNCS style. Authors are strongly encouraged to use LaTeX2e and the Springer llncs class files. If you have difficulties in producing a Springer LNCS style document or you cannot produce postscript or PDF output, please contact cade19sub@tcs.inf.tu-dresden.de.
In addition to papers on foundations (15 pages), we encourage the submission of application papers (10 pages), and of short system descriptions (5 pages). Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed. In the case of doubts on this point please contact the program chair. Papers that are too long will not be considered.
Since the abstract submission phase is over, the electronic abstract submission form is no longer accessible. If you have already submitted an abstract and want to upload your paper, please use the URL that was listed in the (abstract submission) confirmation mail.
| 24th January 2003 | Deadline for electronic submission of title and short abstract |
| 31st January 2003 | Deadline for electronic submission of papers |
| 31st March 2003 | Notification of acceptance of papers |
| 30th April 2003 | Deadline for final versions of accepted papers |
Papers on foundations should present significant and original results that are relevant to automated deduction. The main criterion for inclusion of a paper in the proceedings is whether sufficiently many readers can be expected to profit from reading the paper for their future research in automated deduction. In addition to this general criterion, the reviewers will be asked to evaluate the papers according to the following specific criteria:
RELEVANCE: Is this paper relevant to researchers in automated deduction or does it address issues not relevant for this area? Would it perhaps better be presented at another conference? Is the paper accessible to a general automated deduction audience, or is it only comprehensible for a small segment of the community?
SIGNIFICANCE: How important is the work reported in the paper? Does it attack an important and difficult problem or a peripheral and simple problem? The problem should be interesting and natural, and not just be chosen by the authors because it can be attacked by their methods. Does the approach used to solve the problem advance the state of the art or is it just one more application of a well-known method?
ORIGINALITY: Has this or similar work been previously reported? Are the problems and/or approaches completely new? Is it a novel combination of familiar techniques? Does the paper introduce new approaches and methods, or is it reinventing the wheel using new terminology? The paper should clarify the relationship to previous work. Even if the authors think that previous work in this direction is irrelevant for their work, they should justify their opinion.
QUALITY: Is the paper technically sound? Not only the results but also the proofs must be correct. Does the paper contain enough details to check for correctness? If not, do the authors cite an accessible technical report containing full proofs? In addition to theoretical analysis, empirical evaluations (e.g., of the claim that a certain algorithm behaves good in practice) are also relevant here.
PRESENTATION: Is the paper well organized and well written? The information of the paper should be available to the reader with a minimum of effort. Does the paper cite and discuss previous work? Does it motivate the problem and the approach chosen to solve it? Does it make clear what has been achieved with this paper and what is still to be done? Are definitions crisp and to the point, or does the paper introduce notation after notation without really working with the introduced terminology? Even technical papers on a narrow topic should be written such that non-experts can comprehend the main contribution of the paper and the methods employed. The paper shouldn't just be a litany of deep but obscure theorems.
Papers on applications should present significant and original applications of automated deduction methods and tools. The main criterion for inclusion of a paper in the proceedings is whether sufficiently many readers can be expected to profit from reading the paper for their own application. Thus, it is not enough if all one can learn from the paper is that the authors have an application. Someone with a similar application should be expected to have a considerable advantage after having read the paper. In addition to this general criterion, the reviewers will be asked to evaluate the papers according to the following specific criteria:
RELEVANCE: Is the application built using automated deduction methods, or is it more or less a standard computer science application? Is the use of automated deduction methods justified?
SIGNIFICANCE: How important is the application reported in the paper? Does it involve important and difficult problems or peripheral and simple problems? The application should come from the "real world", and not just be invented by the authors because it can be solved using their methods. If the authors consider a "toy application", what is the purpose? What new insights (e.g., on the behavior of an algorithm) can be gained from considering the toy application? Can one expect the results to generalize to "real world applications"? Does the approach used to build the application advance the state of the art or is it just one more application of a well-known method?
ORIGINALITY: Has this or similar work been previously reported? It is not necessary for the paper to develop new automated deduction techniques, but it should at least apply them in a novel way or shed a new light on their applicability in a certain domain. The paper should clarify the relationship to previous work. Even if the authors think that previous work in this direction is irrelevant for their work, they should justify their opinion.
QUALITY: Is the approach chosen by the authors sound? It is not enough to say that a certain technique has been applied, but it must also be evaluated whether and why this technique worked in the application. The chosen approach should be described in enough detail to allow such an evaluation. Are there empirical evaluations that support the claims made in the paper?
PRESENTATION: Is the paper well organized and well written? The information of the paper should be available to the reader with a minimum of effort. Does the paper cite and discuss previous work? Does it motivate the application and the approach chosen to solve it? Does it make clear what has been achieved with this paper and what is still to be done?
System Descriptions should present an implemented tool and its novel features. A demonstration is expected to accompany a tool presentation. The main criterion for inclusion of a system description is whether sufficiently many readers can profit from reading the paper either for their decision on whether to use the system in their application or for their own implementation work. Thus, it is not enough if all one can learn is that the authors have implemented a system. It should become clear what kind of applications the system has, how it differs from similar systems, and how it behaves on examples or in applications. In addition to this general criterion, the reviewers will be asked to evaluate the system descriptions according to the following specific criteria:
RELEVANCE: Is the system and its description relevant for automated deduction? Does it solve logical inference problems or employ techniques developed in the automated deduction community?
SIGNIFICANCE: How important is the described system? Does it solve important and difficult problems or peripheral and simple ones? The potential application should have a connection to the "real world" and the implemented techniques should be relevant for automated deduction. Is this a mature and optimized implementation or a naive implementation of theoretical techniques? Can new insights be gained from implementing and using this system?
ORIGINALITY: Has a similar system been described before? If yes, what are the novel features reported in the current description? The authors should clarify the relationship to other systems. Why is their system better than other systems? Does the system implement state-of-the-art deduction techniques, or is it based on outdated approaches?
QUALITY: Is the approach chosen by the authors sound? It is not enough to say that certain techniques have been implemented, but it must also be explained why these techniques and their combination are appropriate for the intended applications of the system. The system and its underlying design should be described in enough detail to allow such an evaluation. Are there empirical evaluations that support the claims about the system made in the paper? Is the system available to be tested independently?
PRESENTATION: Is the system description well organized and well written? The information should be available to the reader with a minimum of effort. Does the paper cite and discuss previous work? Does it motivate the design of the system and the intended applications. Does it make clear what has been achieved by the current implementation and what is still to be done?
| Page maintained by Jan Hladik. |