Subversion Repositories wimsdev

!set p_=!word 1 of $wims_read_parm
!bound p_ within none,header,source,html default none
!goto $p_
:none
!exit
:header
!set m_subject=WIMS 3.24: interactive math deductions
!set m_date=20021129
!set m_time=17:02:43
!set m_from=Gang XIAO
!set m_sender_ip=127.0.0.1
!set m_sender_id=
!set m_sender_class=
!set m_email=xiao@unice.fr
!set m_to=
!set m_prec=O200211/1
!set m_exists=yes
!exit
:source
<pre>
The main new feature in version 3.24 is Deductio, an interface for
online interactive mathematics deductions, in particular as exercises.

These interactive deductions may include statement proving, object manipulation (such as linear system reduction or expression simplification), example construction, and more. A Deductio exercise can present a (randomly generated) exercise with hypotheses and objectives, as well as a list of allowed methods which the user can apply to carry step by step deductions untill the objectives are met.
And scores will be attributed according to the efficiency of the deduction process.

For the time being, Deductio is still a first-step partial realisation, with only a very limited number of available methods and a very small number of applications (exercises), mainly for manipulating equations and inequalities. Much more is to be added later, including induction, quantifier processing, variable typing, libraries of theorems, axioms and definitions, methods for groups, rings, non-commutative and/or non-associative structures, etc.

However, it is probably the first time ever there is an interface for
computer-guided deduction that is accessible to the general public. So I am not sure
whether it really meets the demand of the community. And the publication of
this first version is to test the reaction of the users. To put it more
clear, the development of Deductio will soon stop if no interest is shown
from the users' (and contributors') side.

You can make a search for the word &lt;tt>deductio&lt;/tt> in the home page of the server, to get the list of available Deductio exercises.</pre>
!exit
:html
The main new feature in version 3.24 is Deductio, an interface for
online interactive mathematics deductions, in particular as exercises.
<p>
These interactive deductions may include statement proving, object manipulation (such as linear system reduction or expression simplification), example construction, and more. A Deductio exercise can present a (randomly generated) exercise with hypotheses and objectives, as well as a list of allowed methods which the user can apply to carry step by step deductions untill the objectives are met.
And scores will be attributed according to the efficiency of the deduction process.
<p>
For the time being, Deductio is still a first-step partial realisation, with only a very limited number of available methods and a very small number of applications (exercises), mainly for manipulating equations and inequalities. Much more is to be added later, including induction, quantifier processing, variable typing, libraries of theorems, axioms and definitions, methods for groups, rings, non-commutative and/or non-associative structures, etc.
<p>
However, it is probably the first time ever there is an interface for
computer-guided deduction that is accessible to the general public. So I am not sure
whether it really meets the demand of the community. And the publication of
this first version is to test the reaction of the users. To put it more
clear, the development of Deductio will soon stop if no interest is shown
from the users' (and contributors') side.
<p>
You can make a search for the word <tt>deductio</tt> in the home page of the server, to get the list of available Deductio exercises.