Campus Event Calendar
Event Entry
What and Who
An Invitation to Discover REDLOG for Your Work
Thomas Sturm
Uni Passau
Talk RG1 Group Meeting
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 18 January 2008
11:00
30 Minutes
E1 4
Rotunda 6th floor
Saarbrücken
Abstract
REDLOG is a package for the computer algebra system REDUCE. It extends
the idea of symbolic computation from algebraic expressions to
first-order formulas over certain temporarily fixed domains. The range
of currently available domains comprises the complex numbers, the
reals, the linear theory of the integers, the linear theory of p-adic
numbers, queues of real numbers, quantified propositional calculus,
differential algebras, Malcev-type term algebras, and theorem proving
for first-order logic. Some of the REDLOG domains, as e.g. the reals,
are well-established and have numerous applications documented in the
literature, including in particular 3rd-party applications. Others, as
e.g. first-order proving, are rather new and experimental. The talk
starts with an overview over all domains in combination with a brief
introduction to computational quantifier elimination and related
concepts. Next we turn to the REDLOG website, which features besides
other online resources the online database REMIS containing literature
discussing REDLOG examples and corresponding REDLOG input files.
Finally we discuss some ongoing REDLOG projects and developments
planned for the near future. The talk is not going into technical or
mathematical details too much in favor of discussing many different
aspects of REDLOG. One idea is to jointly discover possible REDLOG
applications within the scientific work of the audience, which would
in turn stimulate further improvements of REDLOG.
the idea of symbolic computation from algebraic expressions to
first-order formulas over certain temporarily fixed domains. The range
of currently available domains comprises the complex numbers, the
reals, the linear theory of the integers, the linear theory of p-adic
numbers, queues of real numbers, quantified propositional calculus,
differential algebras, Malcev-type term algebras, and theorem proving
for first-order logic. Some of the REDLOG domains, as e.g. the reals,
are well-established and have numerous applications documented in the
literature, including in particular 3rd-party applications. Others, as
e.g. first-order proving, are rather new and experimental. The talk
starts with an overview over all domains in combination with a brief
introduction to computational quantifier elimination and related
concepts. Next we turn to the REDLOG website, which features besides
other online resources the online database REMIS containing literature
discussing REDLOG examples and corresponding REDLOG input files.
Finally we discuss some ongoing REDLOG projects and developments
planned for the near future. The talk is not going into technical or
mathematical details too much in favor of discussing many different
aspects of REDLOG. One idea is to jointly discover possible REDLOG
applications within the scientific work of the audience, which would
in turn stimulate further improvements of REDLOG.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 01/11/2008 12:12
Roxane Wetzel, 11/05/2007 11:19
Roxane Wetzel, 10/24/2007 14:00 -- Created document.
Roxane Wetzel, 11/05/2007 11:19
Roxane Wetzel, 10/24/2007 14:00 -- Created document.