Both deduction systems and computer algebra systems are receiving growing attention from industry and academia. On the one hand, mathematical software systems have been commercially very successful. Their use is now wide-spread in industry, education, and scientific contexts. On the other hand, the use of formal methods in hardware and software development has made deduction systems indispensable not least because of the complexity and sheer size of the reasoning tasks involved. As many application domains fall outside the scope of existing deduction systems and computer algebra systems, there is still need for improvement and in particular need for the integration of computer algebra and deduction systems.
The JSC special issue is intended for researchers and developers interested in combining the reasoning capabilities of deduction systems and the computational power of computer algebra systems.
Topics of interest include all aspects related to the combination of automated reasoning systems and computer algebra systems:
- Integration/combination of computer algebra systems/algorithms and automated reasoning systems/algorithms
- Incorporation of automated reasoning techniques in computer algebra
- Incorporation of computer algebra techniques in automated reasoning
Typical relevant topics in Automated Reasoning are:
- Logics: including propositional, first-order, classical, equational, higher-order, non-classical, constructive, modal, temporal, many-valued, substructural, description, and meta-logics, type theory and set theory.
- Techniques: including model-elimination, tableaux, SAT, sequent calculi, resolution, connection method, inverse method, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, and AI-related methods for deductive systems such as proof planning and proof presentation.
- Applications: including hardware and software development, systems analysis and verification, functional and logic programming, proof carrying code, deductive databases, knowledge representation, computer mathematics, natural language processing, linguistics, planning and other AI areas.
Typical relevant topics in Computer Algebra are:
We explicitly encourage submissions of results from applications and case studies where the integration of automated reasoning and computer algebra is particularly important. In particular, extended versions of high quality papers presented at the CALCULEMUS-2001 symposium will be particularly appreciated.
- Algorithmic mathematics: Algebraic, symbolic, and symbolic-numeric algorithms including: simplification, polynomial and rational function manipulations, algebraic equations, summation and recurrence equations, integration and differential equations, linear algebra, number theory, group computations, and geometric computing.
- Computer science: Theoretical and practical problems in symbolic mathematical manipulation including: computer algebra systems, data structures, computational complexity, problem solving environments, programming languages and libraries for symbolic-numeric-geometric computation, user interfaces, visualization, software architectures, parallel or distributed computing, mapping algorithms to architectures, analysis and benchmarking, automatic differentiation and code generation, automatic theorem proving, mathematical data exchange protocols.
- Applications: Problem treatments incorporating algebraic, symbolic, symbolic-numeric and geometric computation in an essential or novel way, including engineering, economics and finance, architecture, physical and biological sciences, computer sciences, logic, mathematics, statistics, and uses in education.
Prospective contributors are warmly invited to contact the guest editors to discuss the suitability of topics and papers.
Authors are invited to submit full papers up to 20 pages in JSC format describing original results not published elsewhere. Papers shall be submitted electronically by sending an e-mail to the guest editors (which are calculemus2001's chairs) at calculemus2001-chairs@cs.unitn.it, with header "JSC SPECIAL ISSUE SUBMISSION", containing as MIME attachments the file of the paper in postscript format and a compiled submission form. We require the usage of LaTeX, according to the JSC format and style files (see http://www.academicpress.com/www/journal/TeX-uk/LaTeXFP.htm). The Postscript form must be interpretable by Ghostscript, and must use standard fonts, or include the necessary fonts. Authors who cannot meet these requirements should email the guest editors.
All submitted papers will be refereed according to the usual JSC refereeing process.
To aid planning and organization, we would appreciate an email of intent to submit a paper (including the submission form) as early as possible.
Submission of papers:
Notification of acceptance/rejection:
Submission of revised versions:
Publication of special issue:September 28, 2001
January 11, 2002
February 22, 2002
planned before CALCULEMUS-2002
Steve Linton Roberto Sebastiani School of Computer Science,
University of St. Andrews,
North Haugh, St. Andrews, Fife,
KY16 9SS, SCOTLAND
phone: +44 1334 463269
fax: +44 1334 463278
sal@dcs.st-and.ac.ukDept. of Mathematics,
University of Trento
Via Sommarive 14, I-38050,
Trento, Italy
phone: +39 0461 881514
fax: +39 0461 881624
rseba@science.unitn.it